Theory examples

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


theory examples


imports

  disjoint_relations

begin

section ‹Examples›
subsection ‹Compositions of non-basic relations›
text‹Basic relations are the 13 time interval relations. The unions of basic relations are also relations and their compositions is the union of compositions.
We prove few of these compositions that are required in theory nest.thy.›

method (in arelations) e_compose = (match conclusion in "e O b ⊆ _"   ⇒ ‹insert ceb, blast›  
                                      ¦ _ ⇒ ‹match conclusion in "e O m ⊆ _"  ⇒ ‹insert cem, blast› ¦ _ ⇒ ‹fail››)

declare [[simp_trace_depth_limit=4]] 

lemma eovisidifmifiOm:"(e ∪  ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ m¯ ∪ f^-1) O m ⊆ m ∪ ov ∪ f^-1 ∪ d^-1 ∪ s ∪ s¯ ∪ e" 
apply (simp, intro conjI)
  using cem apply blast
    using crm_rules by auto
 

lemma ovsmfidiesiOmi:"(ov ∪ s∪ m  ∪ f^-1 ∪ d^-1 ∪ e ∪ s^-1) O m^-1 ⊆ d^-1 ∪ s^-1 ∪  ov^-1 ∪ m^-1 ∪ f^-1 ∪ f ∪ e "
apply (simp, intro conjI)
  using crmi_rules by auto
 

lemma ovsmfidiesiOm:"(ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯) O m ⊆ b ∪ ov ∪ f^-1 ∪ d^-1 ∪ m "
apply (simp, intro conjI)
  using crm_rules by auto
  

lemma ovsmfidiesiOssie:"(ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯) O (s ∪ s^-1 ∪ e) ⊆ ov ∪ f^-1 ∪ d^-1 ∪ s ∪ e ∪ s^-1 ∪ m "
apply (simp, intro conjI)
  using crs_rules apply auto[7]
    using crsi_rules apply auto[7]
      using cre_rules by auto[7]

lemma " (b ∪ m ∪ ov ∪ s ∪ d) O (b ∪ m ∪ ov ∪ s ∪ d) ⊆  b ∪ m ∪ ov ∪ s ∪ d"
apply (simp, intro conjI)
 using crb_rules apply auto[5]
  using crm_rules apply auto[5]
    using crov_rules apply auto[5]
      using crs_rules apply auto[5]
        using crd_rules by auto[5]

lemma ebmovovissifsiddib:"(e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯) O b ⊆ b ∪ m ∪ ov ∪ f^-1 ∪ d^-1"
apply (simp, intro conjI)
   using crb_rules by auto
    

lemma ebmovovissiffiddibmovsd:"(e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯) O ( b ∪ m ∪ ov ∪ s ∪ d) ⊆ (b ∪ m ∪ ov ∪ s ∪ d ∪ f^-1 ∪ d^-1 ∪ ov^-1 ∪ s¯ ∪ f ∪ e) "
apply (simp, intro conjI)
  using crb_rules apply auto[11]
    using crm_rules apply auto[11]
      using crov_rules apply auto[11]
        using crs_rules apply auto[11]
          using crd_rules by auto

lemma difimov:"(d^-1 ∪ f^-1 ∪ ov ∪ e ∪ f ∪ m ∪ b ∪ s^-1 ∪ s) O ( m ∪ ov ∪ s ∪ d ∪ b ∪ f^-1 ∪ f ∪ e) ⊆ ( e ∪ b ∪ m ∪ ov ∪ ov^-1 ∪ s ∪ s^-1 ∪ f ∪ f¯ ∪ d ∪ d¯)"
apply (simp, intro conjI)
  using crm_rules apply auto[9]
    using crov_rules apply auto[9]
      using crs_rules apply auto[9]
        using crd_rules apply auto[9]
          using crb_rules apply auto[9]
            using crfi_rules apply auto[9]
              using crf_rules apply auto[9]
                using cre_rules by auto

lemma difibs:"(d¯ ∪ f¯ ∪ ov ∪ e ∪ f ∪ m ∪ b ∪ s¯ ∪ s) O (b ∪ s ∪ m) ⊆ (b ∪ m ∪ ov ∪ f¯ ∪ d¯ ∪ d ∪ e ∪ s ∪ s¯)"
apply (simp, intro conjI)
  using crb_rules apply auto[9]
    using crs_rules apply auto[9]
      using crm_rules by auto
     
lemma bebmovovissiffiddi:"b O (e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯) ⊆ (b ∪ m ∪ ov ∪ s ∪ d)"
apply (simp, intro conjI)
  using cb_rules by auto[11]

lemma ovsmfidiesi:"(((ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯) O (ov^-1 ∪ s^-1 ∪ m^-1 ∪ f ∪ d ∪ e ∪ s)) ⊆ (s ∪ s^-1 ∪ f ∪ f^-1 ∪ d ∪ d^-1 ∪ e ∪ ov ∪ ov^-1 ∪ m ∪ m^-1))"
apply (simp, intro conjI)
  using crovi_rules apply auto[7]
    using crsi_rules apply auto[7]
      using crmi_rules apply auto[7]
        using crf_rules apply auto[7]
          using crd_rules apply auto[7]
            using cre_rules apply auto[7]  
              using crs_rules by auto                    

lemma piiq:"(p,i) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯ ⟹ (i,q) ∈ ov^-1 ∪ s^-1 ∪ m^-1 ∪ f ∪ d ∪ e ∪ s ⟹ (p,q) ∈ s ∪ s^-1 ∪ f ∪ f^-1 ∪ d ∪ d^-1 ∪ e ∪ ov ∪ ov^-1 ∪ m ∪ m^-1"     
using ovsmfidiesi relcomp.relcompI subsetCE by blast      


lemma  ceovisidiffimi_ffie:"(e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯) O (f ∪ f¯ ∪ e) ⊆  e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯ "    
apply (simp, intro conjI)
  using crf_rules apply auto[7]
    using crfi_rules apply auto[7]
      using cre_rules  by auto

lemma  ceovisidiffimi_ffie_simp:"(p,i) ∈ (e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯) ⟹ (i, q) ∈ (f ∪ f¯ ∪ e) ⟹ (p,q) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯ "    
using ceovisidiffimi_ffie relcomp.relcompI subsetCE by blast      

lemma ceovisidiffimi_fife:" (e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯) O (f¯ ∪ f ∪ e)  ⊆  e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯"
apply (simp, intro conjI)
 using cefi covifi csifi cdifi cffi  cfifi cmifi covifi csifi cdifi apply auto[7]
   using cef covif csif cdif cff cfif cmif apply auto[7]
     using cee covie csie cdie cfe cfie cmie by auto[7]
           
lemma "(x, j) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯ ⟹ (j, i) ∈ f¯ ∪ f ∪ e ⟹ (x, i) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯"
using ceovisidiffimi_ffie_simp by blast

lemma m_ovsmfidiesi:"m O (ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯) ⊆ b ∪ s ∪ m"
apply (simp, intro conjI)
 using cm_rules by auto

lemma ovsmfidiesi_d:"(ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯) O d ⊆  e ∪  s ∪ d ∪ ov ∪ ov^-1 ∪ s^-1 ∪ f ∪ f^-1  ∪ d^-1"
apply (simp, intro conjI)
  using crd_rules by auto[7]
    

lemma cbi_esdovovisiffidi:"b^-1 O (e ∪ s ∪ d ∪ ov ∪ ov¯ ∪ s¯ ∪ f ∪ f¯ ∪ d¯) ⊆ b^-1 ∪ m^-1 ∪ ov^-1 ∪ f ∪ d "
apply (simp, intro conjI)
  using cbi_rules by auto[9]
   
lemma cm_alpha1ialpha4mi:"m O  (e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯) ⊆  m ∪ ov ∪ s ∪ d ∪ b ∪ f^-1 ∪ f ∪ e"
apply (simp, intro conjI)
using cm_rules by auto


lemma cbi_alpha1ialpha4mi:"b^-1 O ( e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯) ⊆  b^-1"
apply (simp, intro conjI)
  using cbi_rules by auto

lemma cbeta2_beta2:"( b ∪ m ∪ ov ∪ f¯ ∪ d¯) O ( b ∪ m ∪ ov ∪ f¯ ∪ d¯) ⊆  b ∪ m ∪ ov ∪ f¯ ∪ d¯"
apply (simp, intro conjI)
  using crb_rules apply auto[5]
    using crm_rules apply auto[5]
      using crov_rules apply auto[5]
        using crfi_rules apply auto[5]
          using crdi_rules by auto

lemma cbeta2_gammabm: "(b ∪ m ∪ ov ∪ f¯ ∪ d¯) O ( e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯) ⊆ ( e ∪ b ∪ m ∪ ov ∪ ov¯ ∪ s ∪ s¯ ∪ f ∪ f¯ ∪ d ∪ d¯)"
apply (simp, intro conjI)
  using cre_rules apply auto[5]
    using crb_rules apply auto[5]
      using crm_rules apply auto[5]
        using crov_rules apply auto[5]
          using crovi_rules apply auto[5]
            using crs_rules apply auto[5]
              using crsi_rules apply auto[5]
                using crf_rules apply auto[5]
                  using crfi_rules apply auto[5]
                    using crd_rules apply auto[5]
                      using crdi_rules by auto

lemma calpha1_alpha1:"(b ∪ m ∪ ov ∪ s ∪ d) O ( b ∪ m ∪ ov ∪ s ∪ d) ⊆ ( b ∪ m ∪ ov ∪ s ∪ d)"
apply (simp, intro conjI)
  using crb_rules apply auto[5]
    using crm_rules apply auto[5]
      using crov_rules apply auto[5]
        using crs_rules apply auto[5]
          using crd_rules by auto
   
subsection ‹Intersection of non-basic relations›

lemma  inter_ov:
assumes  "(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)" 
shows "(i,j) ∈ ov"
using assms apply auto 
 using b_rules apply auto[43]
  using e_rules apply auto[9]
   using b_rules apply auto[30]
    using m_rules apply auto[24]
     using b_rules apply auto[6]
      using m_rules apply auto[20]
       using f_rules apply auto[14]
        using d_rules by auto

lemma neq_beta2i_alpha2alpha5m:
assumes  "(q, j) ∈ b¯ ∪ d ∪ f ∪ ov¯ ∪ m¯ " and " (q, j) ∈ ov ∪ s ∪ m ∪ f¯ ∪ d¯ ∪ e ∪ s¯" 
shows  False
using assms apply auto
  using b_rules apply auto[7]
    using ov_rules apply auto[4]
      using d_rules apply auto[6]
        using s_rules apply auto[3]
          using f_rules apply auto[5]
            using m_rules apply auto[2]
              using ov_rules apply auto[4]
                using m_rules by auto

lemma neq_bi_alpha1ialpha4mi:
assumes "(q,i) ∈ b^-1" and " (q, i) ∈ e ∪ ov¯ ∪ s¯ ∪ d¯ ∪ f ∪ f¯ ∪ m¯"
shows False
using assms apply auto
  using b_rules by auto


end