src/HOLCF/FOCUS/Stream_adm.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19763 ec18656a2c10
child 24107 fecafd71e758
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
wenzelm@17293
     1
(*  Title:      HOLCF/ex/Stream_adm.thy
wenzelm@11355
     2
    ID:         $Id$
wenzelm@17293
     3
    Author:     David von Oheimb, TU Muenchen
oheimb@11350
     4
*)
oheimb@11350
     5
wenzelm@17293
     6
header {* Admissibility for streams *}
oheimb@11350
     7
wenzelm@17293
     8
theory Stream_adm
wenzelm@17293
     9
imports Stream Continuity
wenzelm@17293
    10
begin
oheimb@11350
    11
wenzelm@19763
    12
definition
wenzelm@21404
    13
  stream_monoP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
wenzelm@19763
    14
  "stream_monoP F = (\<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
wenzelm@19763
    15
                    (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i\<cdot>rt\<cdot>s \<in> P))"
wenzelm@17293
    16
wenzelm@21404
    17
definition
wenzelm@21404
    18
  stream_antiP  :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool" where
wenzelm@19763
    19
  "stream_antiP F = (\<forall>P x. \<exists>Q i.
wenzelm@17293
    20
                (#x  < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
wenzelm@17293
    21
                (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
wenzelm@19763
    22
                (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i\<cdot>rt\<cdot>y \<in> P))))"
wenzelm@17293
    23
wenzelm@21404
    24
definition
wenzelm@21404
    25
  antitonP :: "'a set => bool" where
wenzelm@19763
    26
  "antitonP P = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P)"
wenzelm@17293
    27
wenzelm@17293
    28
huffman@19759
    29
(* ----------------------------------------------------------------------- *)
huffman@19759
    30
huffman@19759
    31
section "admissibility"
huffman@19759
    32
huffman@19759
    33
lemma flatstream_adm_lemma:
huffman@19759
    34
  assumes 1: "chain Y"
huffman@19759
    35
  assumes 2: "!i. P (Y i)"
huffman@19759
    36
  assumes 3: "(!!Y. [| chain Y; !i. P (Y i); !k. ? j. Fin k < #((Y j)::'a::flat stream)|]
huffman@19759
    37
  ==> P(lub (range Y)))"
huffman@19759
    38
  shows "P(lub (range Y))"
huffman@19759
    39
apply (rule increasing_chain_adm_lemma [OF 1 2])
huffman@19759
    40
apply (erule 3, assumption)
huffman@19759
    41
apply (erule thin_rl)
huffman@19759
    42
apply (rule allI)
huffman@19759
    43
apply (case_tac "!j. stream_finite (Y j)")
huffman@19759
    44
apply ( rule chain_incr)
huffman@19759
    45
apply ( rule allI)
huffman@19759
    46
apply ( drule spec)
huffman@19759
    47
apply ( safe)
huffman@19759
    48
apply ( rule exI)
huffman@19759
    49
apply ( rule slen_strict_mono)
huffman@19759
    50
apply (   erule spec)
huffman@19759
    51
apply (  assumption)
huffman@19759
    52
apply ( assumption)
huffman@19759
    53
apply (drule not_ex [THEN iffD1])
huffman@19759
    54
apply (subst slen_infinite)
huffman@19759
    55
apply (erule thin_rl)
huffman@19759
    56
apply (drule spec)
huffman@19759
    57
apply (fold ile_def)
huffman@19759
    58
apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
huffman@19759
    59
apply (simp)
huffman@19759
    60
done
huffman@19759
    61
huffman@19759
    62
huffman@19759
    63
(* should be without reference to stream length? *)
huffman@19759
    64
lemma flatstream_admI: "[|(!!Y. [| chain Y; !i. P (Y i); 
huffman@19759
    65
 !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"
huffman@19759
    66
apply (unfold adm_def)
huffman@19759
    67
apply (intro strip)
huffman@19759
    68
apply (erule (1) flatstream_adm_lemma)
huffman@19759
    69
apply (fast)
huffman@19759
    70
done
huffman@19759
    71
huffman@19759
    72
huffman@19759
    73
(* context (theory "Nat_InFinity");*)
huffman@19759
    74
lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
huffman@19759
    75
apply (rule ile_trans)
huffman@19759
    76
prefer 2
huffman@19759
    77
apply  (assumption)
huffman@19759
    78
apply (simp)
huffman@19759
    79
done
huffman@19759
    80
huffman@19759
    81
lemma stream_monoP2I:
huffman@19759
    82
"!!X. stream_monoP F ==> !i. ? l. !x y. 
huffman@19759
    83
  Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i"
huffman@19759
    84
apply (unfold stream_monoP_def)
huffman@19759
    85
apply (safe)
huffman@19759
    86
apply (rule_tac x="i*ia" in exI)
huffman@19759
    87
apply (induct_tac "ia")
huffman@19759
    88
apply ( simp)
huffman@19759
    89
apply (simp)
huffman@19759
    90
apply (intro strip)
huffman@19759
    91
apply (erule allE, erule all_dupE, drule mp, erule ile_lemma)
huffman@19759
    92
apply (drule_tac P="%x. x" in subst, assumption)
huffman@19759
    93
apply (erule allE, drule mp, rule ile_lemma) back
huffman@19759
    94
apply ( erule ile_trans)
huffman@19759
    95
apply ( erule slen_mono)
huffman@19759
    96
apply (erule ssubst)
huffman@19759
    97
apply (safe)
huffman@19759
    98
apply ( erule (2) ile_lemma [THEN slen_take_lemma3, THEN subst])
huffman@19759
    99
apply (erule allE)
huffman@19759
   100
apply (drule mp)
huffman@19759
   101
apply ( erule slen_rt_mult)
huffman@19759
   102
apply (erule allE)
huffman@19759
   103
apply (drule mp)
huffman@19759
   104
apply (erule monofun_rt_mult)
huffman@19759
   105
apply (drule (1) mp)
huffman@19759
   106
apply (assumption)
huffman@19759
   107
done
huffman@19759
   108
huffman@19759
   109
lemma stream_monoP2_gfp_admI: "[| !i. ? l. !x y. 
huffman@19759
   110
 Fin l <= #x --> (x::'a::flat stream) << y --> x:down_iterate F i --> y:down_iterate F i;
huffman@19759
   111
    down_cont F |] ==> adm (%x. x:gfp F)"
huffman@19759
   112
apply (erule INTER_down_iterate_is_gfp [THEN ssubst]) (* cont *)
huffman@19759
   113
apply (simp (no_asm))
huffman@19759
   114
apply (rule adm_lemmas)
huffman@19759
   115
apply (rule flatstream_admI)
huffman@19759
   116
apply (erule allE)
huffman@19759
   117
apply (erule exE)
huffman@19759
   118
apply (erule allE, erule exE)
huffman@19759
   119
apply (erule allE, erule allE, drule mp) (* stream_monoP *)
huffman@19759
   120
apply ( drule ileI1)
huffman@19759
   121
apply ( drule ile_trans)
huffman@19759
   122
apply (  rule ile_iSuc)
huffman@19759
   123
apply ( drule iSuc_ile_mono [THEN iffD1])
huffman@19759
   124
apply ( assumption)
huffman@19759
   125
apply (drule mp)
huffman@19759
   126
apply ( erule is_ub_thelub)
huffman@19759
   127
apply (fast)
huffman@19759
   128
done
huffman@19759
   129
huffman@19759
   130
lemmas fstream_gfp_admI = stream_monoP2I [THEN stream_monoP2_gfp_admI]
huffman@19759
   131
huffman@19759
   132
lemma stream_antiP2I:
huffman@19759
   133
"!!X. [|stream_antiP (F::(('a::flat stream)set => ('a stream set)))|]
huffman@19759
   134
  ==> !i x y. x << y --> y:down_iterate F i --> x:down_iterate F i"
huffman@19759
   135
apply (unfold stream_antiP_def)
huffman@19759
   136
apply (rule allI)
huffman@19759
   137
apply (induct_tac "i")
huffman@19759
   138
apply ( simp)
huffman@19759
   139
apply (simp)
huffman@19759
   140
apply (intro strip)
huffman@19759
   141
apply (erule allE, erule all_dupE, erule exE, erule exE)
huffman@19759
   142
apply (erule conjE)
huffman@19759
   143
apply (case_tac "#x < Fin i")
huffman@19759
   144
apply ( fast)
huffman@19759
   145
apply (fold ile_def)
huffman@19759
   146
apply (drule (1) mp)
huffman@19759
   147
apply (erule all_dupE, drule mp, rule refl_less)
huffman@19759
   148
apply (erule ssubst)
huffman@19759
   149
apply (erule allE, drule (1) mp)
huffman@19759
   150
apply (drule_tac P="%x. x" in subst, assumption)
huffman@19759
   151
apply (erule conjE, rule conjI)
huffman@19759
   152
apply ( erule slen_take_lemma3 [THEN ssubst], assumption)
huffman@19759
   153
apply ( assumption)
huffman@19759
   154
apply (erule allE, erule allE, drule mp, erule monofun_rt_mult)
huffman@19759
   155
apply (drule (1) mp)
huffman@19759
   156
apply (assumption)
huffman@19759
   157
done
huffman@19759
   158
huffman@19759
   159
lemma stream_antiP2_non_gfp_admI:
huffman@19759
   160
"!!X. [|!i x y. x << y --> y:down_iterate F i --> x:down_iterate F i; down_cont F |] 
huffman@19759
   161
  ==> adm (%u. ~ u:gfp F)"
huffman@19759
   162
apply (unfold adm_def)
huffman@19759
   163
apply (simp add: INTER_down_iterate_is_gfp)
huffman@19759
   164
apply (fast dest!: is_ub_thelub)
huffman@19759
   165
done
huffman@19759
   166
huffman@19759
   167
lemmas fstream_non_gfp_admI = stream_antiP2I [THEN stream_antiP2_non_gfp_admI]
huffman@19759
   168
huffman@19759
   169
huffman@19759
   170
huffman@19759
   171
(**new approach for adm********************************************************)
huffman@19759
   172
huffman@19759
   173
section "antitonP"
huffman@19759
   174
huffman@19759
   175
lemma antitonPD: "[| antitonP P; y:P; x<<y |] ==> x:P"
huffman@19759
   176
apply (unfold antitonP_def)
huffman@19759
   177
apply auto
huffman@19759
   178
done
huffman@19759
   179
huffman@19759
   180
lemma antitonPI: "!x y. y:P --> x<<y --> x:P ==> antitonP P"
huffman@19759
   181
apply (unfold antitonP_def)
huffman@19759
   182
apply (fast)
huffman@19759
   183
done
huffman@19759
   184
huffman@19759
   185
lemma antitonP_adm_non_P: "antitonP P ==> adm (%u. u~:P)"
huffman@19759
   186
apply (unfold adm_def)
huffman@19759
   187
apply (auto dest: antitonPD elim: is_ub_thelub)
huffman@19759
   188
done
huffman@19759
   189
huffman@19759
   190
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> 
huffman@19759
   191
  adm (\<lambda>u. u\<notin>P)"
huffman@19759
   192
apply (simp)
huffman@19759
   193
apply (rule antitonP_adm_non_P)
huffman@19759
   194
apply (rule antitonPI)
huffman@19759
   195
apply (drule gfp_upperbound)
huffman@19759
   196
apply (fast)
huffman@19759
   197
done
huffman@19759
   198
huffman@19759
   199
lemma adm_set:
huffman@19759
   200
"{lub (range Y) |Y. chain Y & (\<forall>i. Y i \<in> P)} \<subseteq> P \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
huffman@19759
   201
apply (unfold adm_def)
huffman@19759
   202
apply (fast)
huffman@19759
   203
done
huffman@19759
   204
huffman@19759
   205
lemma def_gfp_admI: "P \<equiv> gfp F \<Longrightarrow> {lub (range Y) |Y. chain Y \<and> (\<forall>i. Y i \<in> P)} \<subseteq> 
huffman@19759
   206
  F {lub (range Y) |Y. chain Y \<and> (\<forall>i. Y i \<in> P)} \<Longrightarrow> adm (\<lambda>x. x\<in>P)"
huffman@19759
   207
apply (simp)
huffman@19759
   208
apply (rule adm_set)
huffman@19759
   209
apply (erule gfp_upperbound)
huffman@19759
   210
done
huffman@19759
   211
oheimb@11350
   212
end