src/HOL/HOLCF/FOCUS/Stream_adm.thy
author hoelzl
Tue Jul 19 14:37:09 2011 +0200 (2011-07-19)
changeset 43921 e8511be08ddd
parent 43919 a7e4fb1a0502
child 43924 1165fe965da8
permissions -rw-r--r--
Introduce infinity type class
     1 (*  Title:      HOL/HOLCF/FOCUS/Stream_adm.thy
     2     Author:     David von Oheimb, TU Muenchen
     3 *)
     4 
     5 header {* Admissibility for streams *}
     6 
     7 theory Stream_adm
     8 imports "~~/src/HOL/HOLCF/Library/Stream" "~~/src/HOL/Library/Continuity"
     9 begin
    10 
    11 definition
    12   stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
    13   "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
    14                     (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))"
    15 
    16 definition
    17   stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
    18   "stream_antiP F = (\<forall>P x. \<exists>Q i.
    19                 (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
    20                 (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
    21                 (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))"
    22 
    23 definition
    24   antitonP :: "'a set => bool" where
    25   "antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)"
    26 
    27 
    28 (* ----------------------------------------------------------------------- *)
    29 
    30 section "admissibility"
    31 
    32 lemma infinite_chain_adm_lemma:
    33   "\<lbrakk>Porder.chain Y; \<forall>i. P (Y i);  
    34     \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
    35       \<Longrightarrow> P (\<Squnion>i. Y i)"
    36 apply (case_tac "finite_chain Y")
    37 prefer 2 apply fast
    38 apply (unfold finite_chain_def)
    39 apply safe
    40 apply (erule lub_finch1 [THEN lub_eqI, THEN ssubst])
    41 apply assumption
    42 apply (erule spec)
    43 done
    44 
    45 lemma increasing_chain_adm_lemma:
    46   "\<lbrakk>Porder.chain Y;  \<forall>i. P (Y i); \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i);
    47     \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
    48       \<Longrightarrow> P (\<Squnion>i. Y i)"
    49 apply (erule infinite_chain_adm_lemma)
    50 apply assumption
    51 apply (erule thin_rl)
    52 apply (unfold finite_chain_def)
    53 apply (unfold max_in_chain_def)
    54 apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
    55 done
    56 
    57 lemma flatstream_adm_lemma:
    58   assumes 1: "Porder.chain Y"
    59   assumes 2: "!i. P (Y i)"
    60   assumes 3: "(!!Y. [| Porder.chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
    61   ==> P(LUB i. Y i))"
    62   shows "P(LUB i. Y i)"
    63 apply (rule increasing_chain_adm_lemma [of _ P, OF 1 2])
    64 apply (erule 3, assumption)
    65 apply (erule thin_rl)
    66 apply (rule allI)
    67 apply (case_tac "!j. stream_finite (Y j)")
    68 apply ( rule chain_incr)
    69 apply ( rule allI)
    70 apply ( drule spec)
    71 apply ( safe)
    72 apply ( rule exI)
    73 apply ( rule slen_strict_mono)
    74 apply (   erule spec)
    75 apply (  assumption)
    76 apply ( assumption)
    77 apply (metis enat_ord_code(4) slen_infinite)
    78 done
    79 
    80 (* should be without reference to stream length? *)
    81 lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
    82  !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(LUB i. Y i))|]==> adm P"
    83 apply (unfold adm_def)
    84 apply (intro strip)
    85 apply (erule (1) flatstream_adm_lemma)
    86 apply (fast)
    87 done
    88 
    89 
    90 (* context (theory "Extended_Nat");*)
    91 lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
    92   by (rule order_trans) auto
    93 
    94 lemma stream_monoP2I:
    95 "!!X. stream_monoP F ==> !i. ? l. !x y. 
    96   Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
    97 apply (unfold stream_monoP_def)
    98 apply (safe)
    99 apply (rule_tac x="i*ia" in exI)
   100 apply (induct_tac "ia")
   101 apply ( simp)
   102 apply (simp)
   103 apply (intro strip)
   104 apply (erule allE, erule all_dupE, drule mp, erule ile_lemma)
   105 apply (drule_tac P="%x. x" in subst, assumption)
   106 apply (erule allE, drule mp, rule ile_lemma) back
   107 apply ( erule order_trans)
   108 apply ( erule slen_mono)
   109 apply (erule ssubst)
   110 apply (safe)
   111 apply ( erule (2) ile_lemma [THEN slen_take_lemma3, THEN subst])
   112 apply (erule allE)
   113 apply (drule mp)
   114 apply ( erule slen_rt_mult)
   115 apply (erule allE)
   116 apply (drule mp)
   117 apply (erule monofun_rt_mult)
   118 apply (drule (1) mp)
   119 apply (assumption)
   120 done
   121 
   122 lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
   123  Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
   124     down_cont F |] ==> adm (%x. x:gfp F)"
   125 apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
   126 apply (simp (no_asm))
   127 apply (rule adm_lemmas)
   128 apply (rule flatstream_admI)
   129 apply (erule allE)
   130 apply (erule exE)
   131 apply (erule allE, erule exE)
   132 apply (erule allE, erule allE, drule mp) (* stream_monoP *)
   133 apply ( drule ileI1)
   134 apply ( drule order_trans)
   135 apply (  rule ile_iSuc)
   136 apply ( drule iSuc_ile_mono [THEN iffD1])
   137 apply ( assumption)
   138 apply (drule mp)
   139 apply ( erule is_ub_thelub)
   140 apply (fast)
   141 done
   142 
   143 lemmas fstream_gfp_admI = stream_monoP2I [THEN stream_monoP2_gfp_admI]
   144 
   145 lemma stream_antiP2I:
   146 "!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]
   147   ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i"
   148 apply (unfold stream_antiP_def)
   149 apply (rule allI)
   150 apply (induct_tac "i")
   151 apply ( simp)
   152 apply (simp)
   153 apply (intro strip)
   154 apply (erule allE, erule all_dupE, erule exE, erule exE)
   155 apply (erule conjE)
   156 apply (case_tac "#x < Fin i")
   157 apply ( fast)
   158 apply (unfold linorder_not_less)
   159 apply (drule (1) mp)
   160 apply (erule all_dupE, drule mp, rule below_refl)
   161 apply (erule ssubst)
   162 apply (erule allE, drule (1) mp)
   163 apply (drule_tac P="%x. x" in subst, assumption)
   164 apply (erule conjE, rule conjI)
   165 apply ( erule slen_take_lemma3 [THEN ssubst], assumption)
   166 apply ( assumption)
   167 apply (erule allE, erule allE, drule mp, erule monofun_rt_mult)
   168 apply (drule (1) mp)
   169 apply (assumption)
   170 done
   171 
   172 lemma stream_antiP2_non_gfp_admI:
   173 "!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] 
   174   ==> adm (%u. ~ u:gfp F)"
   175 apply (unfold adm_def)
   176 apply (simp add: INTER_down_iterate_is_gfp)
   177 apply (fast dest!: is_ub_thelub)
   178 done
   179 
   180 lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI]
   181 
   182 
   183 
   184 (**new approach for adm********************************************************)
   185 
   186 section "antitonP"
   187 
   188 lemma antitonPD: "[| antitonP P; y:P; x<<y |] ==> x:P"
   189 apply (unfold antitonP_def)
   190 apply auto
   191 done
   192 
   193 lemma antitonPI: "!x y. y:P --> x<<y --> x:P ==> antitonP P"
   194 apply (unfold antitonP_def)
   195 apply (fast)
   196 done
   197 
   198 lemma antitonP_adm_non_P: "antitonP P ==> adm (%u. u~:P)"
   199 apply (unfold adm_def)
   200 apply (auto dest: antitonPD elim: is_ub_thelub)
   201 done
   202 
   203 lemma def_gfp_adm_nonP: "P \<equiv> gfp F \<Longrightarrow> {y. \<exists>x::'a::pcpo. y \<sqsubseteq> x \<and> x \<in> P} \<subseteq> F {y. \<exists>x. y \<sqsubseteq> x \<and> x \<in> P} \<Longrightarrow> 
   204   adm (\<lambda>u. u\<notin>P)"
   205 apply (simp)
   206 apply (rule antitonP_adm_non_P)
   207 apply (rule antitonPI)
   208 apply (drule gfp_upperbound)
   209 apply (fast)
   210 done
   211 
   212 lemma adm_set:
   213 "{\<Squnion>i. Y i |Y. Porder.chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
   214 apply (unfold adm_def)
   215 apply (fast)
   216 done
   217 
   218 lemma def_gfp_admI: "P \<equiv> gfp F \<Longrightarrow> {\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> 
   219   F {\<Squnion>i. Y i |Y. Porder.chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
   220 apply (simp)
   221 apply (rule adm_set)
   222 apply (erule gfp_upperbound)
   223 done
   224 
   225 end