author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 62175 8ffc4d0e652d child 67613 ce654b0e6d69 permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/HOLCF/FOCUS/Buffer_adm.thy
```
```     2     Author:     David von Oheimb, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section \<open>One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility\<close>
```
```     6
```
```     7 theory Buffer_adm
```
```     8 imports Buffer Stream_adm
```
```     9 begin
```
```    10
```
```    11 declare enat_0 [simp]
```
```    12
```
```    13 lemma BufAC_Asm_d2: "a\<leadsto>s:BufAC_Asm ==> ? d. a=Md d"
```
```    14 by (drule BufAC_Asm_unfold [THEN iffD1], auto)
```
```    15
```
```    16 lemma BufAC_Asm_d3:
```
```    17     "a\<leadsto>b\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\<bullet> & s:BufAC_Asm"
```
```    18 by (drule BufAC_Asm_unfold [THEN iffD1], auto)
```
```    19
```
```    20 lemma BufAC_Asm_F_def3:
```
```    21  "(s:BufAC_Asm_F A) = (s=<> |
```
```    22   (? d. ft\<cdot>s=Def(Md d)) & (rt\<cdot>s=<> | ft\<cdot>(rt\<cdot>s)=Def \<bullet> & rt\<cdot>(rt\<cdot>s):A))"
```
```    23 by (unfold BufAC_Asm_F_def, auto)
```
```    24
```
```    25 lemma cont_BufAC_Asm_F: "inf_continuous BufAC_Asm_F"
```
```    26 by (auto simp add: inf_continuous_def BufAC_Asm_F_def3)
```
```    27
```
```    28 lemma BufAC_Cmt_F_def3:
```
```    29  "((s,t):BufAC_Cmt_F C) = (!d x.
```
```    30     (s = <>       --> t = <>                   ) &
```
```    31     (s = Md d\<leadsto><>  --> t = <>                   ) &
```
```    32     (s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x,rt\<cdot>t):C))"
```
```    33 apply (unfold BufAC_Cmt_F_def)
```
```    34 apply (subgoal_tac "!d x. (s = Md d\<leadsto>\<bullet>\<leadsto>x --> (? y. t = d\<leadsto>y & (x,y):C)) =
```
```    35                      (s = Md d\<leadsto>\<bullet>\<leadsto>x --> ft\<cdot>t = Def d & (x,rt\<cdot>t):C)")
```
```    36 apply (simp)
```
```    37 apply (auto intro: surjectiv_scons [symmetric])
```
```    38 done
```
```    39
```
```    40 lemma cont_BufAC_Cmt_F: "inf_continuous BufAC_Cmt_F"
```
```    41 by (auto simp add: inf_continuous_def BufAC_Cmt_F_def3)
```
```    42
```
```    43
```
```    44 (**** adm_BufAC_Asm ***********************************************************)
```
```    45
```
```    46 lemma BufAC_Asm_F_stream_monoP: "stream_monoP BufAC_Asm_F"
```
```    47 apply (unfold BufAC_Asm_F_def stream_monoP_def)
```
```    48 apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
```
```    49 apply (rule_tac x="Suc (Suc 0)" in exI)
```
```    50 apply (clarsimp)
```
```    51 done
```
```    52
```
```    53 lemma adm_BufAC_Asm: "adm (%x. x:BufAC_Asm)"
```
```    54 apply (unfold BufAC_Asm_def)
```
```    55 apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_monoP [THEN fstream_gfp_admI]])
```
```    56 done
```
```    57
```
```    58
```
```    59 (**** adm_non_BufAC_Asm *******************************************************)
```
```    60
```
```    61 lemma BufAC_Asm_F_stream_antiP: "stream_antiP BufAC_Asm_F"
```
```    62 apply (unfold stream_antiP_def BufAC_Asm_F_def)
```
```    63 apply (intro strip)
```
```    64 apply (rule_tac x="{x. (? d. x = Md d\<leadsto>\<bullet>\<leadsto><>)}" in exI)
```
```    65 apply (rule_tac x="Suc (Suc 0)" in exI)
```
```    66 apply (rule conjI)
```
```    67 prefer 2
```
```    68 apply ( intro strip)
```
```    69 apply ( drule slen_mono)
```
```    70 apply ( drule (1) order_trans)
```
```    71 apply (force)+
```
```    72 done
```
```    73
```
```    74 lemma adm_non_BufAC_Asm: "adm (%u. u~:BufAC_Asm)"
```
```    75 apply (unfold BufAC_Asm_def)
```
```    76 apply (rule cont_BufAC_Asm_F [THEN BufAC_Asm_F_stream_antiP [THEN fstream_non_gfp_admI]])
```
```    77 done
```
```    78
```
```    79 (**** adm_BufAC ***************************************************************)
```
```    80
```
```    81 (*adm_non_BufAC_Asm*)
```
```    82 lemma BufAC_Asm_cong [rule_format]: "!f ff. f:BufEq --> ff:BufEq --> s:BufAC_Asm --> f\<cdot>s = ff\<cdot>s"
```
```    83 apply (rule fstream_ind2)
```
```    84 apply (simp add: adm_non_BufAC_Asm)
```
```    85 apply   (force dest: Buf_f_empty)
```
```    86 apply  (force dest!: BufAC_Asm_d2
```
```    87               dest: Buf_f_d elim: ssubst)
```
```    88 apply (safe dest!: BufAC_Asm_d3)
```
```    89 apply (drule Buf_f_d_req)+
```
```    90 apply (fast elim: ssubst)
```
```    91 done
```
```    92
```
```    93 (*adm_non_BufAC_Asm,BufAC_Asm_cong*)
```
```    94 lemma BufAC_Cmt_d_req:
```
```    95 "!!X. [|f:BufEq; s:BufAC_Asm; (s, f\<cdot>s):BufAC_Cmt|] ==> (a\<leadsto>b\<leadsto>s, f\<cdot>(a\<leadsto>b\<leadsto>s)):BufAC_Cmt"
```
```    96 apply (rule BufAC_Cmt_unfold [THEN iffD2])
```
```    97 apply (intro strip)
```
```    98 apply (frule Buf_f_d_req)
```
```    99 apply (auto elim: BufAC_Asm_cong [THEN subst])
```
```   100 done
```
```   101
```
```   102 (*adm_BufAC_Asm*)
```
```   103 lemma BufAC_Asm_antiton: "antitonP BufAC_Asm"
```
```   104 apply (rule antitonPI)
```
```   105 apply (rule allI)
```
```   106 apply (rule fstream_ind2)
```
```   107 apply (  rule adm_lemmas)+
```
```   108 apply (   rule cont_id)
```
```   109 apply (   rule adm_BufAC_Asm)
```
```   110 apply (  safe)
```
```   111 apply (  rule BufAC_Asm_empty)
```
```   112 apply ( force dest!: fstream_prefix
```
```   113               dest: BufAC_Asm_d2 intro: BufAC_Asm_d)
```
```   114 apply ( force dest!: fstream_prefix
```
```   115               dest: BufAC_Asm_d3 intro!: BufAC_Asm_d_req)
```
```   116 done
```
```   117
```
```   118 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong*)
```
```   119 lemma BufAC_Cmt_2stream_monoP: "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> enat (l i) < #x -->
```
```   120                      (x,f\<cdot>x):(BufAC_Cmt_F ^^ i) top -->
```
```   121                      (s,f\<cdot>s):(BufAC_Cmt_F ^^ i) top"
```
```   122 apply (rule_tac x="%i. 2*i" in exI)
```
```   123 apply (rule allI)
```
```   124 apply (induct_tac "i")
```
```   125 apply ( simp)
```
```   126 apply (simp add: add.commute)
```
```   127 apply (intro strip)
```
```   128 apply (subst BufAC_Cmt_F_def3)
```
```   129 apply (drule_tac P="%x. x" in BufAC_Cmt_F_def3 [THEN subst])
```
```   130 apply safe
```
```   131 apply (   erule Buf_f_empty)
```
```   132 apply (  erule Buf_f_d)
```
```   133 apply ( drule Buf_f_d_req)
```
```   134 apply ( safe, erule ssubst, simp)
```
```   135 apply clarsimp
```
```   136 apply (rename_tac i d xa ya t)
```
```   137 (*
```
```   138  1. \<And>i d xa ya t.
```
```   139        \<lbrakk>f \<in> BufEq;
```
```   140           \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
```
```   141                 x \<sqsubseteq> s \<longrightarrow>
```
```   142                 enat (2 * i) < #x \<longrightarrow>
```
```   143                 (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
```
```   144                 (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
```
```   145           Md d\<leadsto>\<bullet>\<leadsto>xa \<in> BufAC_Asm; enat (2 * i) < #ya; f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>t;
```
```   146           (ya, t) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa\<rbrakk>
```
```   147        \<Longrightarrow> (xa, rt\<cdot>(f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>xa))) \<in> down_iterate BufAC_Cmt_F i
```
```   148 *)
```
```   149 apply (rotate_tac 2)
```
```   150 apply (drule BufAC_Asm_prefix2)
```
```   151 apply (frule Buf_f_d_req, erule exE, erule conjE, rotate_tac -1, erule ssubst)
```
```   152 apply (frule Buf_f_d_req, erule exE, erule conjE)
```
```   153 apply (            subgoal_tac "f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya")
```
```   154 prefer 2
```
```   155 apply ( assumption)
```
```   156 apply (            rotate_tac -1)
```
```   157 apply (            simp)
```
```   158 apply (erule subst)
```
```   159 (*
```
```   160  1. \<And>i d xa ya t ff ffa.
```
```   161        \<lbrakk>f\<cdot>(Md d\<leadsto>\<bullet>\<leadsto>ya) = d\<leadsto>ffa\<cdot>ya; enat (2 * i) < #ya;
```
```   162           (ya, ffa\<cdot>ya) \<in> down_iterate BufAC_Cmt_F i; ya \<sqsubseteq> xa; f \<in> BufEq;
```
```   163           \<forall>x s. s \<in> BufAC_Asm \<longrightarrow>
```
```   164                 x \<sqsubseteq> s \<longrightarrow>
```
```   165                 enat (2 * i) < #x \<longrightarrow>
```
```   166                 (x, f\<cdot>x) \<in> down_iterate BufAC_Cmt_F i \<longrightarrow>
```
```   167                 (s, f\<cdot>s) \<in> down_iterate BufAC_Cmt_F i;
```
```   168           xa \<in> BufAC_Asm; ff \<in> BufEq; ffa \<in> BufEq\<rbrakk>
```
```   169        \<Longrightarrow> (xa, ff\<cdot>xa) \<in> down_iterate BufAC_Cmt_F i
```
```   170 *)
```
```   171 apply (drule spec, drule spec, drule (1) mp)
```
```   172 apply (drule (1) mp)
```
```   173 apply (drule (1) mp)
```
```   174 apply (erule impE)
```
```   175 apply ( subst BufAC_Asm_cong, assumption)
```
```   176 prefer 3 apply assumption
```
```   177 apply assumption
```
```   178 apply ( erule (1) BufAC_Asm_antiton [THEN antitonPD])
```
```   179 apply (subst BufAC_Asm_cong, assumption)
```
```   180 prefer 3 apply assumption
```
```   181 apply assumption
```
```   182 apply assumption
```
```   183 done
```
```   184
```
```   185 lemma BufAC_Cmt_iterate_all: "(x\<in>BufAC_Cmt) = (\<forall>n. x\<in>(BufAC_Cmt_F ^^ n) top)"
```
```   186 apply (unfold BufAC_Cmt_def)
```
```   187 apply (subst cont_BufAC_Cmt_F [THEN inf_continuous_gfp])
```
```   188 apply (fast)
```
```   189 done
```
```   190
```
```   191 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
```
```   192   BufAC_Cmt_2stream_monoP*)
```
```   193 lemma adm_BufAC: "f:BufEq ==> adm (%s. s:BufAC_Asm --> (s, f\<cdot>s):BufAC_Cmt)"
```
```   194 apply (rule flatstream_admI)
```
```   195 apply (subst BufAC_Cmt_iterate_all)
```
```   196 apply (drule BufAC_Cmt_2stream_monoP)
```
```   197 apply safe
```
```   198 apply (drule spec, erule exE)
```
```   199 apply (drule spec, erule impE)
```
```   200 apply  (erule BufAC_Asm_antiton [THEN antitonPD])
```
```   201 apply  (erule is_ub_thelub)
```
```   202 apply (tactic "smp_tac @{context} 3 1")
```
```   203 apply (drule is_ub_thelub)
```
```   204 apply (drule (1) mp)
```
```   205 apply (drule (1) mp)
```
```   206 apply (erule mp)
```
```   207 apply (drule BufAC_Cmt_iterate_all [THEN iffD1])
```
```   208 apply (erule spec)
```
```   209 done
```
```   210
```
```   211
```
```   212
```
```   213 (**** Buf_Eq_imp_AC by induction **********************************************)
```
```   214
```
```   215 (*adm_BufAC_Asm,BufAC_Asm_antiton,adm_non_BufAC_Asm,BufAC_Asm_cong,
```
```   216   BufAC_Cmt_2stream_monoP,adm_BufAC,BufAC_Cmt_d_req*)
```
```   217 lemma Buf_Eq_imp_AC: "BufEq <= BufAC"
```
```   218 apply (unfold BufAC_def)
```
```   219 apply (rule subsetI)
```
```   220 apply (simp)
```
```   221 apply (rule allI)
```
```   222 apply (rule fstream_ind2)
```
```   223 back
```
```   224 apply (   erule adm_BufAC)
```
```   225 apply (  safe)
```
```   226 apply (   erule BufAC_Cmt_empty)
```
```   227 apply (  erule BufAC_Cmt_d)
```
```   228 apply ( drule BufAC_Asm_prefix2)
```
```   229 apply ( simp)
```
```   230 apply (fast intro: BufAC_Cmt_d_req BufAC_Asm_prefix2)
```
```   231 done
```
```   232
```
```   233 (**** new approach for admissibility, reduces itself to absurdity *************)
```
```   234
```
```   235 lemma adm_BufAC_Asm': "adm (\<lambda>x. x\<in>BufAC_Asm)"
```
```   236 apply (rule def_gfp_admI)
```
```   237 apply (rule BufAC_Asm_def [THEN eq_reflection])
```
```   238 apply (safe)
```
```   239 apply (unfold BufAC_Asm_F_def)
```
```   240 apply (safe)
```
```   241 apply (erule contrapos_np)
```
```   242 apply (drule fstream_exhaust_eq [THEN iffD1])
```
```   243 apply (clarsimp)
```
```   244 apply (drule (1) fstream_lub_lemma)
```
```   245 apply (clarify)
```
```   246 apply (erule_tac x="j" in all_dupE)
```
```   247 apply (simp)
```
```   248 apply (drule BufAC_Asm_d2)
```
```   249 apply (clarify)
```
```   250 apply (simp)
```
```   251 apply (rule disjCI)
```
```   252 apply (erule contrapos_np)
```
```   253 apply (drule fstream_exhaust_eq [THEN iffD1])
```
```   254 apply (clarsimp)
```
```   255 apply (drule (1) fstream_lub_lemma)
```
```   256 apply (clarsimp)
```
```   257 apply (simp only: ex_simps [symmetric] all_simps [symmetric])
```
```   258 apply (rule_tac x="Xa" in exI)
```
```   259 apply (rule allI)
```
```   260 apply (rotate_tac -1)
```
```   261 apply (erule_tac x="i" in allE)
```
```   262 apply (clarsimp)
```
```   263 apply (erule_tac x="jb" in allE)
```
```   264 apply (clarsimp)
```
```   265 apply (erule_tac x="jc" in allE)
```
```   266 apply (clarsimp dest!: BufAC_Asm_d3)
```
```   267 done
```
```   268
```
```   269 lemma adm_non_BufAC_Asm': "adm (\<lambda>u. u \<notin> BufAC_Asm)" (* uses antitonP *)
```
```   270 apply (rule def_gfp_adm_nonP)
```
```   271 apply (rule BufAC_Asm_def [THEN eq_reflection])
```
```   272 apply (unfold BufAC_Asm_F_def)
```
```   273 apply (safe)
```
```   274 apply (erule contrapos_np)
```
```   275 apply (drule fstream_exhaust_eq [THEN iffD1])
```
```   276 apply (clarsimp)
```
```   277 apply (frule fstream_prefix)
```
```   278 apply (clarsimp)
```
```   279 apply (frule BufAC_Asm_d2)
```
```   280 apply (clarsimp)
```
```   281 apply (rotate_tac -1)
```
```   282 apply (erule contrapos_pp)
```
```   283 apply (drule fstream_exhaust_eq [THEN iffD1])
```
```   284 apply (clarsimp)
```
```   285 apply (frule fstream_prefix)
```
```   286 apply (clarsimp)
```
```   287 apply (frule BufAC_Asm_d3)
```
```   288 apply (force)
```
```   289 done
```
```   290
```
```   291 lemma adm_BufAC': "f \<in> BufEq \<Longrightarrow> adm (\<lambda>u. u \<in> BufAC_Asm \<longrightarrow> (u, f\<cdot>u) \<in> BufAC_Cmt)"
```
```   292 apply (rule triv_admI)
```
```   293 apply (clarify)
```
```   294 apply (erule (1) Buf_Eq_imp_AC_lemma)
```
```   295       (* this is what we originally aimed to show, using admissibilty :-( *)
```
```   296 done
```
```   297
```
```   298 end
```
```   299
```