(* Title: ZF/UNITY/State.thy
Author: Sidi O Ehmety, Computer Laboratory
Copyright 2001 University of Cambridge
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\<open>UNITY Program States\<close>
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"
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)
(* Union *)
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)
(* Intersection *)
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
(* Diff *)
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
(* Introduction and destruction rules for st_set *)
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)
(*For using "disjunction" (union over an index set) to eliminate a variable.*)
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
