Theory axioms

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



theory axioms

imports
    Main  xor_cal

begin


section ‹Axioms›

text‹We formalize Allen's definition of theory of time in term of intervals (Allen, 1983). 
Two relations, namely meets and equality, are defined between intervals. Two interval meets if they  are adjacent 
A set of 5 axioms ((M1) $\sim$ (M5)) are then defined based on relation meets.›

text‹We define a class interval whose assumptions are (i) properties of relations meets  and, (ii) axioms (M1) $\sim$ (M5).›

class interval =
 fixes
  meets::"'a ⇒ 'a ⇒ bool"  (infixl ‹∥› 60) and
  ℐ::"'a ⇒ bool"
 assumes
  meets_atrans:"⟦(p∥q);(q∥r)⟧ ⟹ ¬(p∥r)" and
  meets_irrefl:"ℐ p ⟹ ¬(p∥p)" and
  meets_asym:"(p∥q) ⟹ ¬(q∥p)" and
  meets_wd:"p∥q ⟹ ℐ p ∧ ℐ q" and
(**** Time axioms ******)
  M1:"⟦(p∥q); (p∥s); (r∥q)⟧ ⟹ (r∥s)" and
  M2:"⟦(p∥q) ; (r∥s)⟧ ⟹ p∥s ⊕ ((∃t. (p∥t)∧(t∥s)) ⊕ (∃t. (r∥t)∧(t∥q)))" and
  M3:"ℐ p ⟹ (∃q r. q∥p ∧ p∥r)" and
  M4:"⟦p∥q ; q∥s ; p∥r ; r∥s⟧ ⟹ q = r"  and
  M5exist:"p∥q ⟹ (∃r s t. r∥p ∧ p∥q ∧ q∥s ∧ r∥t ∧ t∥s)" 
(**********)

lemma  (in interval) trans2:"⟦p∥t; t∥r; r∥q⟧ ⟹ ¬p∥q"
  using M1 meets_asym by blast

lemma (in interval) nontrans1: "u∥r ⟹ ¬ (∃t. u∥t ∧ t∥r)"
  using meets_atrans by blast
 
lemma (in interval) nontrans2:"u∥r ⟹ ¬ (∃t. r∥t ∧ t∥u)"
  using M1 M5exist trans2 by blast

lemma (in interval) nonmeets1:"¬ (u∥r ∧ r∥u)" 
  using meets_asym by blast

lemma (in interval)  nonmeets2: "⟦ℐ u ; ℐ r ⟧ ⟹ ¬ (u∥r ∧ u = r)" 
  using meets_irrefl by blast

lemma (in interval) nonmeets3: "¬ (u∥r ∧ (∃p. u∥p ∧ p∥r))" 
  using nontrans1 by blast

lemma (in interval) nonmeets4: "¬(u∥r ∧ (∃p. r∥p ∧ p∥u))" 
  using nontrans2 by blast

lemma (in interval) elimmeets: "(p ∥ s ∧ (∃t. p ∥ t ∧ t ∥ s) ∧ (∃t. r ∥ t ∧ t ∥ q)) = False"
  using meets_atrans by blast 

lemma (in interval) M5exist_var:
assumes "x∥y" "y∥z" "z∥w"
shows "∃t. x∥t ∧ t∥w"
proof -
  from assms(1,3) have a:"x∥w ⊕ (∃t. x∥t ∧ t∥w) ⊕ (∃t. z∥t ∧ t∥y)" using M2[of x y z w] by auto
  from assms have b1:"¬x∥w" using trans2 by blast
  from assms(2) have "¬ (∃t. z∥t ∧ t∥y)" by (simp add: nontrans2)
  with b1 a have " (∃t. x∥t ∧ t∥w)" by simp
  thus ?thesis by simp
qed

lemma (in interval) M5exist_var2:
assumes "p∥q"
shows "∃r1 r2 r3 s t. r1∥r2 ∧ r2∥r3 ∧ r3∥p ∧ p∥q ∧ q∥s ∧ r1∥t ∧ t∥s"
proof -
  from assms obtain r3 k1 s  where r3p:"r3∥p" and  qs:"q∥s"  and  r3k1:"r3 ∥k1"  and  k1s:"k1∥s" using M5exist by blast 
  from r3p obtain r2 where r2r3:"r2∥r3" using M3[of r3] meets_wd by auto
  from r2r3 obtain r1 where r1r2:"r1∥r2" using M3[of r2] meets_wd by auto
  with  assms  r2r3 r3p qs obtain t where r1t1:"r1∥t" and t1q:"t∥s" using M5exist_var by blast
  with assms r1r2 r2r3 r3p qs show ?thesis by blast
qed
  
lemma (in interval) M5exist_var3:
assumes "k∥l" and "l∥q" and "q∥t" and "t∥r" 
shows  "∃lqt. k∥lqt ∧ lqt∥r"
proof -
  from assms(1-3) obtain lq where "k∥lq" and "lq∥t" 
  using M5exist_var by blast 
  with assms(4) obtain lqt where "k∥lqt" and "lqt∥r" 
  using M5exist_var by blast
  thus ?thesis by auto
qed


end