Theory State
section‹UNITY Program States›
theory State imports ZF begin
consts var :: i
datatype var = Var("i ∈ list(nat)")
type_intros nat_subset_univ [THEN list_subset_univ, THEN subsetD]
consts
type_of :: "i⇒i"
default_val :: "i⇒i"
definition
"state ≡ ∏x ∈ var. cons(default_val(x), type_of(x))"
definition
"st0 ≡ λx ∈ var. default_val(x)"
definition
st_set :: "i⇒o" where
"st_set(A) ≡ A<=state"
definition
st_compl :: "i⇒i" where
"st_compl(A) ≡ state-A"
lemma st0_in_state [simp,TC]: "st0 ∈ state"
by (simp add: state_def st0_def)
lemma st_set_Collect [iff]: "st_set({x ∈ state. P(x)})"
by (simp add: st_set_def, auto)
lemma st_set_0 [iff]: "st_set(0)"
by (simp add: st_set_def)
lemma st_set_state [iff]: "st_set(state)"
by (simp add: st_set_def)
lemma st_set_Un_iff [iff]: "st_set(A ∪ B) ⟷ st_set(A) ∧ st_set(B)"
by (simp add: st_set_def, auto)
lemma st_set_Union_iff [iff]: "st_set(⋃(S)) ⟷ (∀A ∈ S. st_set(A))"
by (simp add: st_set_def, auto)
lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ⟹ st_set(A ∩ B)"
by (simp add: st_set_def, auto)
lemma st_set_Inter [intro!]:
"(S=0) | (∃A ∈ S. st_set(A)) ⟹ st_set(⋂(S))"
apply (simp add: st_set_def Inter_def, auto)
done
lemma st_set_DiffI [intro!]: "st_set(A) ⟹ st_set(A - B)"
by (simp add: st_set_def, auto)
lemma Collect_Int_state [simp]: "Collect(state,P) ∩ state = Collect(state,P)"
by auto
lemma state_Int_Collect [simp]: "state ∩ Collect(state,P) = Collect(state,P)"
by auto
lemma st_setI: "A ⊆ state ⟹ st_set(A)"
by (simp add: st_set_def)
lemma st_setD: "st_set(A) ⟹ A<=state"
by (simp add: st_set_def)
lemma st_set_subset: "⟦st_set(A); B<=A⟧ ⟹ st_set(B)"
by (simp add: st_set_def, auto)
lemma state_update_type:
"⟦s ∈ state; x ∈ var; y ∈ type_of(x)⟧ ⟹ s(x:=y):state"
apply (simp add: state_def)
apply (blast intro: update_type)
done
lemma st_set_compl [simp]: "st_set(st_compl(A))"
by (simp add: st_compl_def, auto)
lemma st_compl_iff [simp]: "x ∈ st_compl(A) ⟷ x ∈ state ∧ x ∉ A"
by (simp add: st_compl_def)
lemma st_compl_Collect [simp]:
"st_compl({s ∈ state. P(s)}) = {s ∈ state. ¬P(s)}"
by (simp add: st_compl_def, auto)
lemma UN_conj_eq:
"∀d∈D. f(d) ∈ A ⟹ (⋃k∈A. {d∈D. P(d) ∧ f(d) = k}) = {d∈D. P(d)}"
by blast
end