Theory Adjacency

theory Adjacency 

imports QSizeR QSizeO RBG TORL TMTL

begin

consts

rAdj :: "Rg => Rg => o"

Adj :: "Ob => Ob => Ti => o"
pAdj :: "Ob => Ob => o"
Att :: "Ob => Ob => o"

defs

rAdj_def: "rAdj(a,b) ==  ~CGR(a,b) &  (EX c. (SpR(c) & NEGR(c,a) & NEGR(c,b) &  CGR(c,a) & CGR(c,b)))"

Adj_def: "Adj(x,y,t) == (EX a b . (L(x,a,t) & L(y,b,t) & rAdj(a,b)))"
pAdj_def: "pAdj(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> Adj(x,y,t)))"

Att_def: "Att(x,y) ==  pDC(x,y) & (EX z1 z2. (pPP(z1,x) & pPP(z2,y) & pNEG(z1,x) & pNEG(z2,y) & pAdj(z1,z2)))" 



(* theorems for region adjacency *)

theorem rAdj_irrefl: "ALL a. (~rAdj(a,a))"
apply(rule allI)
apply(unfold rAdj_def)
apply(insert CGR_refl)
apply(auto)
done

theorem rAdj_sym: "rAdj(a,b) ==> rAdj(b,a)"
apply(unfold rAdj_def)
apply(insert CGR_sym)
apply(auto)
done


theorem rAdj_and_PR_and_PR_and_notCGR_imp_rAdj: "[|rAdj(a,b);PR(a,aa);PR(b,bb);~CGR(aa,bb)|] ==> rAdj(aa,bb)"
apply(unfold rAdj_def)
apply(safe)
apply(rule_tac x="c" in exI)
apply(safe)
apply(drule_tac a="c" and b="a" and c="aa" in NEGR_and_PR_imp_NEGR)
apply(assumption)
apply(assumption)
apply(drule_tac a="c" and b="b" and c="bb" in NEGR_and_PR_imp_NEGR)
apply(assumption)
apply(assumption)
apply(drule_tac a="a" and b="aa" in PR_imp_CGR_imp_CGR)
apply(erule_tac x="c" in allE)
apply(safe)
apply(drule_tac a="b" and b="bb" in PR_imp_CGR_imp_CGR)
apply(erule_tac x="c" in allE)
apply(safe)
done 




(* theorems for adjacency and attachment *)

theorem Adj_irrefl: "ALL x t. (~Adj(x,x,t))"
apply(rule allI,rule allI)
apply(unfold Adj_def)
apply(safe)
apply(drule_tac x="x" and a="a" and b="b" and t="t" in L_unique)
apply(auto)
apply(insert rAdj_irrefl)
apply(auto)
done

theorem Adj_sym: "Adj(x,y,t) ==> Adj(y,x,t)"
apply(unfold Adj_def)
apply(safe)
apply(rule_tac x="b" in exI)
apply(rule_tac x="a" in exI)
apply(insert rAdj_sym)
apply(auto)
done

theorem Adj_imp_notC: "Adj(x,y,t) ==> ~C(x,y,t)"
apply(unfold Adj_def)
apply(clarify)
apply(unfold C_def)
apply(clarify)
apply(drule_tac x="x" and a="a" and b="aa" and t="t" in  L_unique)
apply(assumption)
apply(drule_tac x="y" and a="b" and b="ba" and t="t" in  L_unique)
apply(assumption)
apply(unfold rAdj_def)
apply(auto)
done

theorem Adj_exists: "Adj(x,y,t) ==> (E(x,t) & E(y,t))"
apply(unfold Adj_def)
apply(safe)
apply(rule L_exists2)
apply(auto)
apply(rule L_exists2)
apply(auto)
done

theorem Adj_and_P_and_P_and_notC_imp_Adj: "[|Adj(x,y,t);P(x,xx,t);P(y,yy,t);~C(xx,yy,t)|] ==> Adj(xx,yy,t)"
apply(unfold Adj_def)
apply(clarify)
apply(frule_tac x="x" and y="xx" and t="t" in P_exists2_rule)
apply(frule_tac x="y" and y="yy" and t="t" in P_exists2_rule)
apply(clarify)
apply(drule_tac x="xx" and t="t" in L_exists1)
apply(drule_tac x="yy" and t="t" in L_exists1)
apply(clarify)
apply(rule_tac x="aa" in exI)
apply(rule_tac x="ab" in exI)
apply(safe)
thm rAdj_and_PR_and_PR_and_notCGR_imp_rAdj
apply(rule_tac a="a" and b="b" and aa="aa" and bb="ab" in  rAdj_and_PR_and_PR_and_notCGR_imp_rAdj)
apply(safe)
apply(drule_tac x="x" and y="xx" and t="t" and a="a" and b="aa" in L_P_PR_rule)
apply(assumption)
apply(assumption)
apply(assumption)
apply(drule_tac x="y" and y="yy" and t="t" and a="b" and b="ab" in L_P_PR_rule)
apply(assumption)
apply(assumption)
apply(assumption)
apply(unfold C_def)
apply(auto)
done 


theorem pAdj_and_pP_and_pP_and_pDC_imp_pAdj: "[|pAdj(x,y);pP(x,xx);pP(y,yy);pDC(xx,yy)|] ==> pAdj(xx,yy)"
apply(drule_tac x="xx" and y="yy" in pDC_imp_notC)
apply(unfold pAdj_def, unfold pP_def)
apply(clarify)
apply(rule  Adj_and_P_and_P_and_notC_imp_Adj)
apply(auto)
apply(erule_tac x="t" in allE)
apply(auto)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule P_exists2_rule)
apply(safe)
apply(erule_tac x="t" in allE)
apply(safe)
apply(rotate_tac 1)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule P_exists2_rule)
apply(erule conjE)
apply(clarify)
apply(rotate_tac 2)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule P_exists2_rule)
apply(clarify)
apply(rotate_tac 1)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule Adj_exists)
apply(auto)
apply(rotate_tac 1)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule P_exists2_rule)
apply(clarify)
apply(rotate_tac 3)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule Adj_exists)
apply(auto)
done


theorem pAdj_irrefl: "ALL x. (~pAdj(x,x))"
apply(unfold pAdj_def)
apply(insert P_exists1)
apply(insert Adj_irrefl)
apply(auto)
done


theorem pAdj_sym: "pAdj(x,y) ==> pAdj(y,x)"
apply(unfold pAdj_def)
apply(insert Adj_sym)
apply(auto)
done



theorem Att_imp_pAdj: "Att(x,y) ==> pAdj(x,y)"
apply(unfold Att_def)
apply(clarify)
apply(drule_tac x="z1" and y="x" in pPP_imp_pP_and_notpP)
apply(drule_tac x="z2" and y="y" in pPP_imp_pP_and_notpP)
apply(rule pAdj_and_pP_and_pP_and_pDC_imp_pAdj)
apply(auto)
done


theorem Att_sym: "Att(x,y) ==> Att(y,x)"
apply(unfold Att_def)
apply(safe)
apply(drule pDC_sym)
apply(safe)
apply(drule pAdj_sym)
apply(rule_tac x="z2" in exI)
apply(rule_tac x="z1" in exI)
apply(clarify)
done

theorem Att_irrefl: "(ALL x. ~Att(x,x))"
apply(unfold Att_def)
apply(insert pDC_irrefl)
apply(auto)
done 



end