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