1(*  Title:      ZF/UNITY/State.thy
2    Author:     Sidi O Ehmety, Computer Laboratory
3    Copyright   2001  University of Cambridge
4
5Formalizes UNITY-program states using dependent types so that:
6 - variables are typed.
7 - the state space is uniform, common to all defined programs.
8 - variables can be quantified over.
9*)
10
11section\<open>UNITY Program States\<close>
12
13theory State imports ZF begin
14
15consts var :: i
16datatype var = Var("i \<in> list(nat)")
17  type_intros  nat_subset_univ [THEN list_subset_univ, THEN subsetD]
18
19consts
20  type_of :: "i=>i"
21  default_val :: "i=>i"
22
23definition
24  "state == \<Prod>x \<in> var. cons(default_val(x), type_of(x))"
25
26definition
27  "st0 == \<lambda>x \<in> var. default_val(x)"
28  
29definition
30  st_set  :: "i=>o"  where
31(* To prevent typing conditions like `A<=state' from
32   being used in combination with the rules `constrains_weaken', etc. *)
33  "st_set(A) == A<=state"
34
35definition
36  st_compl :: "i=>i"  where
37  "st_compl(A) == state-A"
38
39
40lemma st0_in_state [simp,TC]: "st0 \<in> state"
41by (simp add: state_def st0_def)
42
43lemma st_set_Collect [iff]: "st_set({x \<in> state. P(x)})"
44by (simp add: st_set_def, auto)
45
46lemma st_set_0 [iff]: "st_set(0)"
47by (simp add: st_set_def)
48
49lemma st_set_state [iff]: "st_set(state)"
50by (simp add: st_set_def)
51
52(* Union *)
53
54lemma st_set_Un_iff [iff]: "st_set(A \<union> B) \<longleftrightarrow> st_set(A) & st_set(B)"
55by (simp add: st_set_def, auto)
56
57lemma st_set_Union_iff [iff]: "st_set(\<Union>(S)) \<longleftrightarrow> (\<forall>A \<in> S. st_set(A))"
58by (simp add: st_set_def, auto)
59
60(* Intersection *)
61
62lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ==> st_set(A \<inter> B)"
63by (simp add: st_set_def, auto)
64
65lemma st_set_Inter [intro!]: 
66   "(S=0) | (\<exists>A \<in> S. st_set(A)) ==> st_set(\<Inter>(S))"
67apply (simp add: st_set_def Inter_def, auto)
68done
69
70(* Diff *)
71lemma st_set_DiffI [intro!]: "st_set(A) ==> st_set(A - B)"
72by (simp add: st_set_def, auto)
73
74lemma Collect_Int_state [simp]: "Collect(state,P) \<inter> state = Collect(state,P)"
75by auto
76
77lemma state_Int_Collect [simp]: "state \<inter> Collect(state,P) = Collect(state,P)"
78by auto
79
80
81(* Introduction and destruction rules for st_set *)
82
83lemma st_setI: "A \<subseteq> state ==> st_set(A)"
84by (simp add: st_set_def)
85
86lemma st_setD: "st_set(A) ==> A<=state"
87by (simp add: st_set_def)
88
89lemma st_set_subset: "[| st_set(A); B<=A |] ==> st_set(B)"
90by (simp add: st_set_def, auto)
91
92
93lemma state_update_type: 
94     "[| s \<in> state; x \<in> var; y \<in> type_of(x) |] ==> s(x:=y):state"
95apply (simp add: state_def)
96apply (blast intro: update_type)
97done
98
99lemma st_set_compl [simp]: "st_set(st_compl(A))"
100by (simp add: st_compl_def, auto)
101
102lemma st_compl_iff [simp]: "x \<in> st_compl(A) \<longleftrightarrow> x \<in> state & x \<notin> A"
103by (simp add: st_compl_def)
104
105lemma st_compl_Collect [simp]:
106     "st_compl({s \<in> state. P(s)}) = {s \<in> state. ~P(s)}"
107by (simp add: st_compl_def, auto)
108
109(*For using "disjunction" (union over an index set) to eliminate a variable.*)
110lemma UN_conj_eq:
111     "\<forall>d\<in>D. f(d) \<in> A ==> (\<Union>k\<in>A. {d\<in>D. P(d) & f(d) = k}) = {d\<in>D. P(d)}"
112by blast
113
114end
115