Theory jointly_exhaustive

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



theory jointly_exhaustive

imports
  allen

begin

section ‹JE property›
text ‹The 13 time interval relations are jointly exhaustive. For any two intervals $x$ and $y$, we can find a basic relation $r$ such that $(x,y) \in r$.›
 
lemma (in arelations) jointly_exhaustive:
assumes  "ℐ p" "ℐ q"
shows "(p::'a,q::'a) ∈ b ∨ (p,q) ∈ m ∨ (p,q) ∈ ov ∨ (p,q) ∈ s ∨ (p,q) ∈ d ∨ (p,q) ∈ f^-1 ∨ (p,q) ∈ e ∨ 
                                    (p,q) ∈ f ∨ (p,q) ∈ s^-1 ∨ (p,q) ∈ d^-1 ∨ (p,q) ∈ ov^-1 ∨ (p,q) ∈ m^-1 ∨ (p,q) ∈ b^-1 " (is ?R)
proof -
  obtain k k' u u'::'a where kp:"k∥p" and kpq:"k'∥q" and pu:"p∥u" and qup:"q∥u'" using M3 meets_wd assms(1,2) by fastforce
  from kp kpq have "k∥q ⊕ ((∃t. k∥t ∧ t∥q) ⊕ (∃t. k'∥t ∧ t∥p))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
  then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
  thus ?thesis
  proof (elim disjE)
      { assume "?A∧¬?B∧¬?C" then have kq:?A by simp
        from pu qup have "p∥u' ⊕ ((∃t'::'a. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "(?A∧¬?B∧¬?C)" then have "?A" by simp
           with kp kq qup have "p = q" using M4 by auto
           thus ?thesis using  e  by auto}
          next
          {assume "¬?A∧?B∧¬?C" then have "?B" by simp
           with kq kp qup show ?thesis using  s by blast}
          next
          {assume "(¬?A∧¬?B∧?C)" then have "?C" by simp
           then obtain t' where "q∥t'" and "t'∥u" by blast
           with kq kp pu show ?thesis using  s by blast }
        qed}
      next
      { assume "¬?A∧?B∧¬?C" then have ?B by simp
        then obtain t where kt:"k∥t" and tq:"t∥q" by auto
        from pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with kp qup kt tq show ?thesis using f  by blast}
          next
          {assume "¬?A∧?B∧¬?C"  then have ?B by simp
           then obtain t' where ptp:"p∥t'" and tpup:"t'∥u'" by auto
           from pu tq  have "p∥q ⊕ ((∃t''. p∥t'' ∧ t''∥q) ⊕ (∃t''. t∥t'' ∧ t''∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using  m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using  b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then have ?C by simp
                then obtain g where "t∥g" and "g∥u" by auto
                moreover with pu ptp have "g∥t'" using M1 by blast
                ultimately  show ?thesis using  ov kt tq kp ptp tpup qup   by blast}
           qed}
         next
          {assume "¬?A∧¬?B∧?C" then have ?C by simp
           then obtain t' where "q∥t'" and "t'∥u" by auto
           with kp  kt tq pu show ?thesis using d  by blast}
         qed}
      next
      { assume "¬?A∧¬?B∧?C" then have ?C by simp
        then obtain t where kpt:"k'∥t" and tp:"t∥p" by auto
        from  pu qup have "p∥u' ⊕ ((∃t'. p∥t' ∧ t'∥u') ⊕ (∃t'. q∥t' ∧ t'∥u))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
        then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
        thus ?thesis
        proof (elim disjE)
          {assume "?A∧¬?B∧¬?C" then have ?A by simp
           with qup kpt tp kpq show ?thesis using  f by blast}
          next
          {assume "¬?A∧?B∧¬?C" then have ?B by simp
           with qup kpt tp kpq show ?thesis using  d by blast}
          next
          {assume "¬?A∧¬?B∧?C" then obtain t' where qt':"q∥t'" and tpc:"t'∥u" by auto
           from qup tp have "q∥p ⊕ ((∃t''. q∥t'' ∧ t''∥p) ⊕ (∃t''. t∥t'' ∧ t''∥u'))" (is "?A ⊕ (?B ⊕ ?C)") using M2 by blast
           then have "(?A∧¬?B∧¬?C) ∨ ((¬?A∧?B∧¬?C) ∨ (¬?A∧¬?B∧?C))" by (insert xor_distr_L[of ?A ?B ?C], auto simp:elimmeets)
           thus ?thesis
           proof (elim disjE)
              {assume "?A∧¬?B∧¬?C" then have ?A by simp
               thus ?thesis using  m by auto}
              next
              {assume "¬?A∧?B∧¬?C" then have ?B by simp
               thus ?thesis using  b by auto}
              next
              { assume "¬?A∧¬?B∧?C" then obtain g where tg:"t∥g" and "g∥u'" by auto
                with qup qt' have "g∥t'" using M1 by blast
                with qt' tpc pu kpq kpt tp tg show ?thesis using  ov by blast}
          qed}
     qed}
 qed
qed

lemma (in arelations) JE:
assumes "ℐ p" "ℐ q" 
shows "(p::'a,q::'a) ∈ b ∪ m  ∪ ov  ∪ s ∪ d ∪ f^-1 ∪ e ∪ f  ∪ s^-1  ∪ d^-1 ∪ ov^-1 ∪ m^-1  ∪ b^-1 "
using jointly_exhaustive UnCI assms(1,2) by blast


end