# Theory State

theory State
imports ZF
```(*  Title:      ZF/UNITY/State.thy
Author:     Sidi O Ehmety, Computer Laboratory

Formalizes UNITY-program states using dependent types so that:
- variables are typed.
- the state space is uniform, common to all defined programs.
- variables can be quantified over.
*)

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
(* To prevent typing conditions like `A<=state' from
being used in combination with the rules `constrains_weaken', etc. *)
"st_set(A) == A<=state"

definition
st_compl :: "i=>i"  where
"st_compl(A) == state-A"

lemma st0_in_state [simp,TC]: "st0 ∈ state"

lemma st_set_Collect [iff]: "st_set({x ∈ state. P(x)})"

lemma st_set_0 [iff]: "st_set(0)"

lemma st_set_state [iff]: "st_set(state)"

(* Union *)

lemma st_set_Un_iff [iff]: "st_set(A ∪ B) ⟷ st_set(A) & st_set(B)"

lemma st_set_Union_iff [iff]: "st_set(⋃(S)) ⟷ (∀A ∈ S. st_set(A))"

(* Intersection *)

lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ==> st_set(A ∩ B)"

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

(* Diff *)
lemma st_set_DiffI [intro!]: "st_set(A) ==> st_set(A - B)"

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

(* Introduction and destruction rules for st_set *)

lemma st_setI: "A ⊆ state ==> st_set(A)"

lemma st_setD: "st_set(A) ==> A<=state"

lemma st_set_subset: "[| st_set(A); B<=A |] ==> st_set(B)"

lemma state_update_type:
"[| s ∈ state; x ∈ var; y ∈ type_of(x) |] ==> s(x:=y):state"
apply (blast intro: update_type)
done

lemma st_set_compl [simp]: "st_set(st_compl(A))"

lemma st_compl_iff [simp]: "x ∈ st_compl(A) ⟷ x ∈ state & x ∉ A"