Theory Views

theory Views
imports Main
begin

(* structural representation of views *)
record 'e V_rec =
  V :: "'e set"
  N :: "'e set"
  C :: "'e set"

(* syntax abbreviations for V_rec *)
abbreviation VrecV :: "'e V_rec ⇒ 'e set"
("V⇘_⇙" [100] 1000)
where
"V⇘v⇙ ≡ (V v)"

abbreviation VrecN :: "'e V_rec ⇒ 'e set"
("N⇘_⇙" [100] 1000)
where
"N⇘v⇙ ≡ (N v)"

abbreviation VrecC :: "'e V_rec ⇒ 'e set"
("C⇘_⇙" [100] 1000)
where
"C⇘v⇙ ≡ (C v)"

(* side conditions for views *)
definition VN_disjoint :: "'e V_rec ⇒ bool"
where
"VN_disjoint v ≡ V⇘v⇙ ∩ N⇘v⇙ = {}"

definition VC_disjoint :: "'e V_rec ⇒ bool"
where
"VC_disjoint v ≡ V⇘v⇙ ∩ C⇘v⇙ = {}"

definition NC_disjoint :: "'e V_rec ⇒ bool"
where
"NC_disjoint v ≡ N⇘v⇙ ∩ C⇘v⇙ = {}"

(* Views are instances of V_rec that satisfy V_valid. *)
definition V_valid :: "'e V_rec ⇒ bool"
where
"V_valid  v ≡ VN_disjoint v ∧ VC_disjoint v ∧ NC_disjoint v"

(* A view is a view on a set of events iff it covers exactly those events and is a valid view*)
definition isViewOn :: "'e V_rec ⇒ 'e set ⇒ bool" 
where
"isViewOn 𝒱 E ≡ V_valid 𝒱 ∧ V⇘𝒱⇙ ∪ N⇘𝒱⇙ ∪ C⇘𝒱⇙ = E"

end