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