95 definition |
95 definition |
96 BufSt :: "SPEC11" where |
96 BufSt :: "SPEC11" where |
97 "BufSt = {f. \<exists>h\<in>BufSt_P. f = h \<currency>}" |
97 "BufSt = {f. \<exists>h\<in>BufSt_P. f = h \<currency>}" |
98 |
98 |
99 |
99 |
100 lemma set_cong: "!!X. A = B ==> (x:A) = (x:B)" |
100 lemma set_cong: "\<And>X. A = B \<Longrightarrow> (x\<in>A) = (x\<in>B)" |
101 by (erule subst, rule refl) |
101 by (erule subst, rule refl) |
102 |
102 |
103 |
103 |
104 (**** BufEq *******************************************************************) |
104 (**** BufEq *******************************************************************) |
105 |
105 |
106 lemma mono_BufEq_F: "mono BufEq_F" |
106 lemma mono_BufEq_F: "mono BufEq_F" |
107 by (unfold mono_def BufEq_F_def, fast) |
107 by (unfold mono_def BufEq_F_def, fast) |
108 |
108 |
109 lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN eq_reflection, THEN def_gfp_unfold]] |
109 lemmas BufEq_fix = mono_BufEq_F [THEN BufEq_def [THEN eq_reflection, THEN def_gfp_unfold]] |
110 |
110 |
111 lemma BufEq_unfold: "(f:BufEq) = (!d. f\<cdot>(Md d\<leadsto><>) = <> & |
111 lemma BufEq_unfold: "(f\<in>BufEq) = (\<forall>d. f\<cdot>(Md d\<leadsto><>) = <> \<and> |
112 (!x. ? ff:BufEq. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>(ff\<cdot>x)))" |
112 (\<forall>x. \<exists>ff\<in>BufEq. f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>(ff\<cdot>x)))" |
113 apply (subst BufEq_fix [THEN set_cong]) |
113 apply (subst BufEq_fix [THEN set_cong]) |
114 apply (unfold BufEq_F_def) |
114 apply (unfold BufEq_F_def) |
115 apply (simp) |
115 apply (simp) |
116 done |
116 done |
117 |
117 |
118 lemma Buf_f_empty: "f:BufEq \<Longrightarrow> f\<cdot><> = <>" |
118 lemma Buf_f_empty: "f\<in>BufEq \<Longrightarrow> f\<cdot><> = <>" |
119 by (drule BufEq_unfold [THEN iffD1], auto) |
119 by (drule BufEq_unfold [THEN iffD1], auto) |
120 |
120 |
121 lemma Buf_f_d: "f:BufEq \<Longrightarrow> f\<cdot>(Md d\<leadsto><>) = <>" |
121 lemma Buf_f_d: "f\<in>BufEq \<Longrightarrow> f\<cdot>(Md d\<leadsto><>) = <>" |
122 by (drule BufEq_unfold [THEN iffD1], auto) |
122 by (drule BufEq_unfold [THEN iffD1], auto) |
123 |
123 |
124 lemma Buf_f_d_req: |
124 lemma Buf_f_d_req: |
125 "f:BufEq \<Longrightarrow> \<exists>ff. ff:BufEq \<and> f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x" |
125 "f\<in>BufEq \<Longrightarrow> \<exists>ff. ff\<in>BufEq \<and> f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x) = d\<leadsto>ff\<cdot>x" |
126 by (drule BufEq_unfold [THEN iffD1], auto) |
126 by (drule BufEq_unfold [THEN iffD1], auto) |
127 |
127 |
128 |
128 |
129 (**** BufAC_Asm ***************************************************************) |
129 (**** BufAC_Asm ***************************************************************) |
130 |
130 |
132 by (unfold mono_def BufAC_Asm_F_def, fast) |
132 by (unfold mono_def BufAC_Asm_F_def, fast) |
133 |
133 |
134 lemmas BufAC_Asm_fix = |
134 lemmas BufAC_Asm_fix = |
135 mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN eq_reflection, THEN def_gfp_unfold]] |
135 mono_BufAC_Asm_F [THEN BufAC_Asm_def [THEN eq_reflection, THEN def_gfp_unfold]] |
136 |
136 |
137 lemma BufAC_Asm_unfold: "(s:BufAC_Asm) = (s = <> | (? d x. |
137 lemma BufAC_Asm_unfold: "(s\<in>BufAC_Asm) = (s = <> \<or> (\<exists>d x. |
138 s = Md d\<leadsto>x & (x = <> | (ft\<cdot>x = Def \<bullet> & (rt\<cdot>x):BufAC_Asm))))" |
138 s = Md d\<leadsto>x \<and> (x = <> \<or> (ft\<cdot>x = Def \<bullet> \<and> (rt\<cdot>x)\<in>BufAC_Asm))))" |
139 apply (subst BufAC_Asm_fix [THEN set_cong]) |
139 apply (subst BufAC_Asm_fix [THEN set_cong]) |
140 apply (unfold BufAC_Asm_F_def) |
140 apply (unfold BufAC_Asm_F_def) |
141 apply (simp) |
141 apply (simp) |
142 done |
142 done |
143 |
143 |
144 lemma BufAC_Asm_empty: "<> :BufAC_Asm" |
144 lemma BufAC_Asm_empty: "<> \<in> BufAC_Asm" |
145 by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
145 by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
146 |
146 |
147 lemma BufAC_Asm_d: "Md d\<leadsto><>:BufAC_Asm" |
147 lemma BufAC_Asm_d: "Md d\<leadsto><> \<in> BufAC_Asm" |
148 by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
148 by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
149 lemma BufAC_Asm_d_req: "x:BufAC_Asm ==> Md d\<leadsto>\<bullet>\<leadsto>x:BufAC_Asm" |
149 lemma BufAC_Asm_d_req: "x \<in> BufAC_Asm \<Longrightarrow> Md d\<leadsto>\<bullet>\<leadsto>x \<in> BufAC_Asm" |
150 by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
150 by (rule BufAC_Asm_unfold [THEN iffD2], auto) |
151 lemma BufAC_Asm_prefix2: "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> s:BufAC_Asm" |
151 lemma BufAC_Asm_prefix2: "a\<leadsto>b\<leadsto>s \<in> BufAC_Asm ==> s \<in> BufAC_Asm" |
152 by (drule BufAC_Asm_unfold [THEN iffD1], auto) |
152 by (drule BufAC_Asm_unfold [THEN iffD1], auto) |
153 |
153 |
154 |
154 |
155 (**** BBufAC_Cmt **************************************************************) |
155 (**** BBufAC_Cmt **************************************************************) |
156 |
156 |
158 by (unfold mono_def BufAC_Cmt_F_def, fast) |
158 by (unfold mono_def BufAC_Cmt_F_def, fast) |
159 |
159 |
160 lemmas BufAC_Cmt_fix = |
160 lemmas BufAC_Cmt_fix = |
161 mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN eq_reflection, THEN def_gfp_unfold]] |
161 mono_BufAC_Cmt_F [THEN BufAC_Cmt_def [THEN eq_reflection, THEN def_gfp_unfold]] |
162 |
162 |
163 lemma BufAC_Cmt_unfold: "((s,t):BufAC_Cmt) = (!d x. |
163 lemma BufAC_Cmt_unfold: "((s,t) \<in> BufAC_Cmt) = (\<forall>d x. |
164 (s = <> --> t = <>) & |
164 (s = <> \<longrightarrow> t = <>) \<and> |
165 (s = Md d\<leadsto><> --> t = <>) & |
165 (s = Md d\<leadsto><> \<longrightarrow> t = <>) \<and> |
166 (s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x, rt\<cdot>t):BufAC_Cmt))" |
166 (s = Md d\<leadsto>\<bullet>\<leadsto>x \<longrightarrow> ft\<cdot>t = Def d \<and> (x, rt\<cdot>t) \<in> BufAC_Cmt))" |
167 apply (subst BufAC_Cmt_fix [THEN set_cong]) |
167 apply (subst BufAC_Cmt_fix [THEN set_cong]) |
168 apply (unfold BufAC_Cmt_F_def) |
168 apply (unfold BufAC_Cmt_F_def) |
169 apply (simp) |
169 apply (simp) |
170 done |
170 done |
171 |
171 |
172 lemma BufAC_Cmt_empty: "f:BufEq ==> (<>, f\<cdot><>):BufAC_Cmt" |
172 lemma BufAC_Cmt_empty: "f \<in> BufEq \<Longrightarrow> (<>, f\<cdot><>) \<in> BufAC_Cmt" |
173 by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_empty) |
173 by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_empty) |
174 |
174 |
175 lemma BufAC_Cmt_d: "f:BufEq ==> (a\<leadsto>\<bottom>, f\<cdot>(a\<leadsto>\<bottom>)):BufAC_Cmt" |
175 lemma BufAC_Cmt_d: "f \<in> BufEq \<Longrightarrow> (a\<leadsto>\<bottom>, f\<cdot>(a\<leadsto>\<bottom>)) \<in> BufAC_Cmt" |
176 by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_d) |
176 by (rule BufAC_Cmt_unfold [THEN iffD2], auto simp add: Buf_f_d) |
177 |
177 |
178 lemma BufAC_Cmt_d2: |
178 lemma BufAC_Cmt_d2: |
179 "(Md d\<leadsto>\<bottom>, f\<cdot>(Md d\<leadsto>\<bottom>)):BufAC_Cmt ==> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" |
179 "(Md d\<leadsto>\<bottom>, f\<cdot>(Md d\<leadsto>\<bottom>)) \<in> BufAC_Cmt \<Longrightarrow> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" |
180 by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
180 by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
181 |
181 |
182 lemma BufAC_Cmt_d3: |
182 lemma BufAC_Cmt_d3: |
183 "(Md d\<leadsto>\<bullet>\<leadsto>x, f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)):BufAC_Cmt ==> (x, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x))):BufAC_Cmt" |
183 "(Md d\<leadsto>\<bullet>\<leadsto>x, f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)) \<in> BufAC_Cmt \<Longrightarrow> (x, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x))) \<in> BufAC_Cmt" |
184 by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
184 by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
185 |
185 |
186 lemma BufAC_Cmt_d32: |
186 lemma BufAC_Cmt_d32: |
187 "(Md d\<leadsto>\<bullet>\<leadsto>x, f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)):BufAC_Cmt ==> ft\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)) = Def d" |
187 "(Md d\<leadsto>\<bullet>\<leadsto>x, f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)) \<in> BufAC_Cmt \<Longrightarrow> ft\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>x)) = Def d" |
188 by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
188 by (drule BufAC_Cmt_unfold [THEN iffD1], auto) |
189 |
189 |
190 (**** BufAC *******************************************************************) |
190 (**** BufAC *******************************************************************) |
191 |
191 |
192 lemma BufAC_f_d: "f \<in> BufAC \<Longrightarrow> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" |
192 lemma BufAC_f_d: "f \<in> BufAC \<Longrightarrow> f\<cdot>(Md d\<leadsto>\<bottom>) = \<bottom>" |
193 apply (unfold BufAC_def) |
193 apply (unfold BufAC_def) |
194 apply (fast intro: BufAC_Cmt_d2 BufAC_Asm_d) |
194 apply (fast intro: BufAC_Cmt_d2 BufAC_Asm_d) |
195 done |
195 done |
196 |
196 |
197 lemma ex_elim_lemma: "(? ff:B. (!x. f\<cdot>(a\<leadsto>b\<leadsto>x) = d\<leadsto>ff\<cdot>x)) = |
197 lemma ex_elim_lemma: "(\<exists>ff\<in>B. (\<forall>x. f\<cdot>(a\<leadsto>b\<leadsto>x) = d\<leadsto>ff\<cdot>x)) = |
198 ((!x. ft\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x)) = Def d) & (LAM x. rt\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x))):B)" |
198 ((\<forall>x. ft\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x)) = Def d) \<and> (LAM x. rt\<cdot>(f\<cdot>(a\<leadsto>b\<leadsto>x)))\<in>B)" |
199 (* this is an instance (though unification cannot handle this) of |
199 (* this is an instance (though unification cannot handle this) of |
200 lemma "(? ff:B. (!x. f\<cdot>x = d\<leadsto>ff\<cdot>x)) = \ |
200 lemma "(? ff:B. (!x. f\<cdot>x = d\<leadsto>ff\<cdot>x)) = \ |
201 \((!x. ft\<cdot>(f\<cdot>x) = Def d) & (LAM x. rt\<cdot>(f\<cdot>x)):B)"*) |
201 \((!x. ft\<cdot>(f\<cdot>x) = Def d) & (LAM x. rt\<cdot>(f\<cdot>x)):B)"*) |
202 apply safe |
202 apply safe |
203 apply ( rule_tac [2] P="(%x. x:B)" in ssubst) |
203 apply ( rule_tac [2] P="(\<lambda>x. x\<in>B)" in ssubst) |
204 prefer 3 |
204 prefer 3 |
205 apply ( assumption) |
205 apply ( assumption) |
206 apply ( rule_tac [2] cfun_eqI) |
206 apply ( rule_tac [2] cfun_eqI) |
207 apply ( drule_tac [2] spec) |
207 apply ( drule_tac [2] spec) |
208 apply ( drule_tac [2] f="rt" in cfun_arg_cong) |
208 apply ( drule_tac [2] f="rt" in cfun_arg_cong) |
234 by (unfold mono_def BufSt_F_def, fast) |
234 by (unfold mono_def BufSt_F_def, fast) |
235 |
235 |
236 lemmas BufSt_P_fix = |
236 lemmas BufSt_P_fix = |
237 mono_BufSt_F [THEN BufSt_P_def [THEN eq_reflection, THEN def_gfp_unfold]] |
237 mono_BufSt_F [THEN BufSt_P_def [THEN eq_reflection, THEN def_gfp_unfold]] |
238 |
238 |
239 lemma BufSt_P_unfold: "(h:BufSt_P) = (!s. h s\<cdot><> = <> & |
239 lemma BufSt_P_unfold: "(h\<in>BufSt_P) = (\<forall>s. h s\<cdot><> = <> \<and> |
240 (!d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x & |
240 (\<forall>d x. h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x \<and> |
241 (? hh:BufSt_P. h (Sd d)\<cdot>(\<bullet>\<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x))))" |
241 (\<exists>hh\<in>BufSt_P. h (Sd d)\<cdot>(\<bullet>\<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x))))" |
242 apply (subst BufSt_P_fix [THEN set_cong]) |
242 apply (subst BufSt_P_fix [THEN set_cong]) |
243 apply (unfold BufSt_F_def) |
243 apply (unfold BufSt_F_def) |
244 apply (simp) |
244 apply (simp) |
245 done |
245 done |
246 |
246 |
247 lemma BufSt_P_empty: "h:BufSt_P ==> h s \<cdot> <> = <>" |
247 lemma BufSt_P_empty: "h \<in> BufSt_P \<Longrightarrow> h s \<cdot> <> = <>" |
248 by (drule BufSt_P_unfold [THEN iffD1], auto) |
248 by (drule BufSt_P_unfold [THEN iffD1], auto) |
249 lemma BufSt_P_d: "h:BufSt_P ==> h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x" |
249 lemma BufSt_P_d: "h \<in> BufSt_P \<Longrightarrow> h \<currency> \<cdot>(Md d\<leadsto>x) = h (Sd d)\<cdot>x" |
250 by (drule BufSt_P_unfold [THEN iffD1], auto) |
250 by (drule BufSt_P_unfold [THEN iffD1], auto) |
251 lemma BufSt_P_d_req: "h:BufSt_P ==> \<exists>hh\<in>BufSt_P. |
251 lemma BufSt_P_d_req: "h \<in> BufSt_P ==> \<exists>hh\<in>BufSt_P. |
252 h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x)" |
252 h (Sd d)\<cdot>(\<bullet> \<leadsto>x) = d\<leadsto>(hh \<currency> \<cdot>x)" |
253 by (drule BufSt_P_unfold [THEN iffD1], auto) |
253 by (drule BufSt_P_unfold [THEN iffD1], auto) |
254 |
254 |
255 |
255 |
256 (**** Buf_AC_imp_Eq ***********************************************************) |
256 (**** Buf_AC_imp_Eq ***********************************************************) |