Theory DataSpace
section ‹Partitoned Data Spaces for Statecharts›
theory DataSpace
imports Contrib
begin
subsection ‹Definitions›
definition
DataSpace :: "('d set) list
=> bool" where
"DataSpace L = ((distinct L) ∧
(∀ D1∈(set L). ∀ D2∈(set L).
D1 ≠ D2 ⟶ ((D1 ∩ D2) = {})) ∧
((⋃ (set L)) = UNIV))"
lemma DataSpace_EmptySet:
"[UNIV] ∈ { L | L. DataSpace L }"
by (unfold DataSpace_def, auto)
definition "dataspace = { L | (L::('d set) list). DataSpace L}"
typedef 'd dataspace = "dataspace :: 'd set list set"
unfolding dataspace_def
apply (rule exI)
apply (rule DataSpace_EmptySet)
done
definition
PartNum :: "('d)dataspace => nat" where
"PartNum = length o Rep_dataspace"
definition
PartDom :: "['d dataspace, nat] => ('d set)" (infixl ‹!D!› 101) where
"PartDom d n = (Rep_dataspace d) ! n"
subsection ‹Lemmas›
subsubsection ‹‹DataSpace››
lemma DataSpace_UNIV [simp]:
"DataSpace [UNIV]"
by (unfold DataSpace_def, auto)
lemma DataSpace_select:
"DataSpace (Rep_dataspace L)"
apply (cut_tac x=L in Rep_dataspace)
apply (unfold dataspace_def)
apply auto
done
lemma UNIV_dataspace [simp]:
"[UNIV] ∈ dataspace"
by (unfold dataspace_def, auto)
lemma Inl_Inr_DataSpace [simp]:
"DataSpace [Part UNIV Inl, Part UNIV Inr]"
apply (unfold DataSpace_def)
apply auto
apply (rename_tac d)
apply (rule_tac b="(inv Inl) d" in Part_eqI)
apply auto
apply (rule sym)
apply (case_tac d)
apply auto
done
lemma Inl_Inr_dataspace [simp]:
"[Part UNIV Inl, Part UNIV Inr] ∈ dataspace"
by (unfold dataspace_def, auto)
lemma InlInr_InlInl_Inr_DataSpace [simp]:
"DataSpace [Part UNIV (Inl o Inr), Part UNIV (Inl o Inl), Part UNIV Inr]"
apply (unfold DataSpace_def)
apply auto
apply (unfold Part_def)
apply auto
apply (rename_tac x)
apply (case_tac x)
apply auto
apply (rename_tac a)
apply (case_tac a)
apply auto
done
lemma InlInr_InlInl_Inr_dataspace [simp]:
"[Part UNIV (Inl o Inr), Part UNIV (Inl o Inl), Part UNIV Inr] : dataspace"
by (unfold dataspace_def, auto)
subsubsection ‹‹PartNum››
lemma PartDom_PartNum_distinct:
"⟦ i < PartNum d; j < PartNum d;
i ≠ j; p ∈ (d !D! i) ⟧ ⟹
p ∉ (d !D! j)"
apply auto
apply (cut_tac L=d in DataSpace_select)
apply (unfold DataSpace_def)
apply auto
apply (erule_tac x="Rep_dataspace d ! i" in ballE)
apply (erule_tac x="Rep_dataspace d ! j" in ballE)
apply auto
apply (simp add:distinct_conv_nth PartNum_def)
apply (unfold PartDom_def PartNum_def)
apply auto
done
lemma PartDom_PartNum_distinct2:
"⟦ i < PartNum d; j < PartNum d;
i ≠ j; p ∈ (d !D! j) ⟧ ⟹
p ∉ (d !D! i)"
apply auto
apply (cut_tac L=d in DataSpace_select)
apply (unfold DataSpace_def)
apply auto
apply (erule_tac x="Rep_dataspace d ! i" in ballE)
apply (erule_tac x="Rep_dataspace d ! j" in ballE)
apply auto
apply (simp add:distinct_conv_nth PartNum_def)
apply (unfold PartDom_def PartNum_def)
apply auto
done
lemma PartNum_length [simp]:
"(DataSpace L) ⟹ (PartNum (Abs_dataspace L) = (length L))"
apply (unfold PartNum_def)
apply auto
apply (subst Abs_dataspace_inverse)
apply (unfold dataspace_def)
apply auto
done
end