author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
child 58871  c399ae4b836f 
permissions  rwrr 
37936  1 
(* Title: ZF/UNITY/State.thy 
11479  2 
Author: Sidi O Ehmety, Computer Laboratory 
3 
Copyright 2001 University of Cambridge 

4 

12195  5 
Formalizes UNITYprogram states using dependent types so that: 
11479  6 
 variables are typed. 
7 
 the state space is uniform, common to all defined programs. 

8 
 variables can be quantified over. 

9 
*) 

10 

14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

11 
header{*UNITY Program States*} 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

12 

26060  13 
theory State imports Main begin 
11479  14 

14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

15 
consts var :: i 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

16 
datatype var = Var("i \<in> list(nat)") 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

17 
type_intros nat_subset_univ [THEN list_subset_univ, THEN subsetD] 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

18 

11479  19 
consts 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

20 
type_of :: "i=>i" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

21 
default_val :: "i=>i" 
11479  22 

24893  23 
definition 
24 
"state == \<Pi> x \<in> var. cons(default_val(x), type_of(x))" 

14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

25 

24893  26 
definition 
27 
"st0 == \<lambda>x \<in> var. default_val(x)" 

14046  28 

24893  29 
definition 
30 
st_set :: "i=>o" where 

14046  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" 

11479  34 

24893  35 
definition 
36 
st_compl :: "i=>i" where 

14046  37 
"st_compl(A) == stateA" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

38 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

39 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

40 
lemma st0_in_state [simp,TC]: "st0 \<in> state" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

41 
by (simp add: state_def st0_def) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

42 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

43 
lemma st_set_Collect [iff]: "st_set({x \<in> state. P(x)})" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

44 
by (simp add: st_set_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

45 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

46 
lemma st_set_0 [iff]: "st_set(0)" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

47 
by (simp add: st_set_def) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

48 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

49 
lemma st_set_state [iff]: "st_set(state)" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

50 
by (simp add: st_set_def) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

51 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

52 
(* Union *) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

53 

46823  54 
lemma st_set_Un_iff [iff]: "st_set(A \<union> B) \<longleftrightarrow> st_set(A) & st_set(B)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

55 
by (simp add: st_set_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

56 

46823  57 
lemma st_set_Union_iff [iff]: "st_set(\<Union>(S)) \<longleftrightarrow> (\<forall>A \<in> S. st_set(A))" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

58 
by (simp add: st_set_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

59 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

60 
(* Intersection *) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

61 

46823  62 
lemma st_set_Int [intro!]: "st_set(A)  st_set(B) ==> st_set(A \<inter> B)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

63 
by (simp add: st_set_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

64 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

65 
lemma st_set_Inter [intro!]: 
46823  66 
"(S=0)  (\<exists>A \<in> S. st_set(A)) ==> st_set(\<Inter>(S))" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

67 
apply (simp add: st_set_def Inter_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

68 
done 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

69 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

70 
(* Diff *) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

71 
lemma st_set_DiffI [intro!]: "st_set(A) ==> st_set(A  B)" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

72 
by (simp add: st_set_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

73 

46823  74 
lemma Collect_Int_state [simp]: "Collect(state,P) \<inter> state = Collect(state,P)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

75 
by auto 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

76 

46823  77 
lemma state_Int_Collect [simp]: "state \<inter> Collect(state,P) = Collect(state,P)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

78 
by auto 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

79 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

80 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

81 
(* Introduction and destruction rules for st_set *) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

82 

46823  83 
lemma st_setI: "A \<subseteq> state ==> st_set(A)" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

84 
by (simp add: st_set_def) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

85 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

86 
lemma st_setD: "st_set(A) ==> A<=state" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

87 
by (simp add: st_set_def) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

88 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

89 
lemma st_set_subset: "[ st_set(A); B<=A ] ==> st_set(B)" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

90 
by (simp add: st_set_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

91 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

92 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

93 
lemma state_update_type: 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

94 
"[ s \<in> state; x \<in> var; y \<in> type_of(x) ] ==> s(x:=y):state" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

95 
apply (simp add: state_def) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

96 
apply (blast intro: update_type) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

97 
done 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

98 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

99 
lemma st_set_compl [simp]: "st_set(st_compl(A))" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

100 
by (simp add: st_compl_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

101 

46823  102 
lemma st_compl_iff [simp]: "x \<in> st_compl(A) \<longleftrightarrow> x \<in> state & x \<notin> A" 
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

103 
by (simp add: st_compl_def) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

104 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

105 
lemma st_compl_Collect [simp]: 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

106 
"st_compl({s \<in> state. P(s)}) = {s \<in> state. ~P(s)}" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

107 
by (simp add: st_compl_def, auto) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

108 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

109 
(*For using "disjunction" (union over an index set) to eliminate a variable.*) 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

110 
lemma UN_conj_eq: 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

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)}" 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

112 
by blast 
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

113 

ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14046
diff
changeset

114 
end 