src/HOL/HOLCF/FOCUS/Fstream.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62175 8ffc4d0e652d
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
tuned proofs;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/FOCUS/Fstream.thy
wenzelm@17293
     2
    Author:     David von Oheimb, TU Muenchen
oheimb@11350
     3
wenzelm@32960
     4
FOCUS streams (with lifted elements).
wenzelm@32960
     5
wenzelm@32960
     6
TODO: integrate Fstreams.thy
oheimb@11350
     7
*)
oheimb@11350
     8
wenzelm@62175
     9
section \<open>FOCUS flat streams\<close>
oheimb@11350
    10
wenzelm@17293
    11
theory Fstream
wenzelm@41413
    12
imports "~~/src/HOL/HOLCF/Library/Stream"
wenzelm@17293
    13
begin
oheimb@11350
    14
wenzelm@36452
    15
default_sort type
wenzelm@17293
    16
huffman@41476
    17
type_synonym 'a fstream = "'a lift stream"
oheimb@11350
    18
wenzelm@19763
    19
definition
wenzelm@21404
    20
  fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
wenzelm@19763
    21
  "fscons a = (\<Lambda> s. Def a && s)"
oheimb@11350
    22
wenzelm@21404
    23
definition
wenzelm@21404
    24
  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
wenzelm@19763
    25
  "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))"
oheimb@11350
    26
wenzelm@19763
    27
abbreviation
wenzelm@21404
    28
  emptystream   :: "'a fstream"                          ("<>") where
wenzelm@19763
    29
  "<> == \<bottom>"
oheimb@11350
    30
wenzelm@21404
    31
abbreviation
wenzelm@61998
    32
  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_\<leadsto>_)" [66,65] 65) where
wenzelm@61998
    33
  "a\<leadsto>s == fscons a\<cdot>s"
oheimb@11350
    34
wenzelm@21404
    35
abbreviation
wenzelm@61998
    36
  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_\<copyright>_)" [64,63] 63) where
wenzelm@61998
    37
  "A\<copyright>s == fsfilter A\<cdot>s"
oheimb@11350
    38
wenzelm@61998
    39
notation (ASCII)
wenzelm@61998
    40
  fscons'  ("(_~>_)" [66,65] 65) and
wenzelm@61998
    41
  fsfilter'  ("(_'(C')_)" [64,63] 63)
oheimb@11350
    42
oheimb@11350
    43
huffman@19759
    44
lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
huffman@40087
    45
by simp
huffman@19759
    46
huffman@19759
    47
huffman@19759
    48
section "fscons"
huffman@19759
    49
huffman@19759
    50
lemma fscons_def2: "a~>s = Def a && s"
huffman@19759
    51
apply (unfold fscons_def)
huffman@19759
    52
apply (simp)
huffman@19759
    53
done
huffman@19759
    54
huffman@19759
    55
lemma fstream_exhaust: "x = UU |  (? a y. x = a~> y)"
huffman@19759
    56
apply (simp add: fscons_def2)
huffman@35781
    57
apply (cut_tac stream.nchotomy)
huffman@19759
    58
apply (fast dest: not_Undef_is_Def [THEN iffD1])
huffman@19759
    59
done
huffman@19759
    60
huffman@19759
    61
lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
huffman@19759
    62
apply (cut_tac fstream_exhaust)
huffman@19759
    63
apply (erule disjE)
huffman@19759
    64
apply fast
huffman@19759
    65
apply fast
huffman@19759
    66
done
wenzelm@27148
    67
huffman@19759
    68
lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)"
huffman@19759
    69
apply (simp add: fscons_def2 stream_exhaust_eq)
huffman@19759
    70
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
huffman@19759
    71
done
huffman@19759
    72
huffman@19759
    73
huffman@19759
    74
lemma fscons_not_empty [simp]: "a~> s ~= <>"
huffman@19759
    75
by (simp add: fscons_def2)
huffman@19759
    76
huffman@19759
    77
huffman@19759
    78
lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b &  s = t)"
huffman@19759
    79
by (simp add: fscons_def2)
huffman@19759
    80
huffman@19759
    81
lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt &  s << tt"
huffman@35532
    82
apply (cases t)
huffman@19759
    83
apply (cut_tac fscons_not_empty)
huffman@45049
    84
apply (fast dest: bottomI)
huffman@19759
    85
apply (simp add: fscons_def2)
huffman@19759
    86
done
huffman@19759
    87
huffman@19759
    88
lemma fstream_prefix' [simp]:
huffman@19759
    89
        "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))"
huffman@45049
    90
apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix'])
huffman@19759
    91
apply (safe)
huffman@19759
    92
apply (erule_tac [!] contrapos_np)
huffman@19759
    93
prefer 2 apply (fast elim: DefE)
huffman@40009
    94
apply (rule lift.exhaust)
huffman@19759
    95
apply (erule (1) notE)
huffman@19759
    96
apply (safe)
huffman@40431
    97
apply (drule Def_below_Def [THEN iffD1])
huffman@19759
    98
apply fast
huffman@19759
    99
done
huffman@19759
   100
huffman@19759
   101
(* ------------------------------------------------------------------------- *)
huffman@19759
   102
huffman@19759
   103
section "ft & rt"
huffman@19759
   104
huffman@19759
   105
lemmas ft_empty = stream.sel_rews (1)
huffman@19759
   106
lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m"
huffman@19759
   107
by (simp add: fscons_def)
huffman@19759
   108
huffman@19759
   109
lemmas rt_empty = stream.sel_rews (2)
huffman@19759
   110
lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s"
huffman@19759
   111
by (simp add: fscons_def)
huffman@19759
   112
huffman@19759
   113
lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (? t. s = a~> t)"
huffman@19759
   114
apply (unfold fscons_def)
huffman@19759
   115
apply (simp)
huffman@19759
   116
apply (safe)
huffman@19759
   117
apply (erule subst)
huffman@19759
   118
apply (rule exI)
huffman@19759
   119
apply (rule surjectiv_scons [symmetric])
huffman@19759
   120
apply (simp)
huffman@19759
   121
done
huffman@19759
   122
huffman@19759
   123
lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)"
huffman@19759
   124
by auto
huffman@19759
   125
huffman@19759
   126
lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x"
huffman@19759
   127
by (simp add: surjective_fscons_lemma)
huffman@19759
   128
huffman@19759
   129
huffman@19759
   130
(* ------------------------------------------------------------------------- *)
huffman@19759
   131
huffman@19759
   132
section "take"
huffman@19759
   133
huffman@19759
   134
lemma fstream_take_Suc [simp]:
huffman@19759
   135
        "stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s"
huffman@19759
   136
by (simp add: fscons_def)
huffman@19759
   137
huffman@19759
   138
huffman@19759
   139
(* ------------------------------------------------------------------------- *)
huffman@19759
   140
huffman@19759
   141
section "slen"
huffman@19759
   142
huffman@44019
   143
lemma slen_fscons: "#(m~> s) = eSuc (#s)"
huffman@19759
   144
by (simp add: fscons_def)
huffman@19759
   145
huffman@19759
   146
lemma slen_fscons_eq:
hoelzl@43924
   147
        "(enat (Suc n) < #x) = (? a y. x = a~> y & enat n < #y)"
huffman@19759
   148
apply (simp add: fscons_def2 slen_scons_eq)
huffman@19759
   149
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
huffman@19759
   150
done
huffman@19759
   151
huffman@19759
   152
lemma slen_fscons_eq_rev:
hoelzl@43924
   153
        "(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y | #y < enat (Suc n))"
huffman@19759
   154
apply (simp add: fscons_def2 slen_scons_eq_rev)
wenzelm@62175
   155
apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
wenzelm@62175
   156
apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
wenzelm@62175
   157
apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
wenzelm@62175
   158
apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
wenzelm@62175
   159
apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
wenzelm@62175
   160
apply (tactic \<open>step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1\<close>)
huffman@19759
   161
apply (erule contrapos_np)
huffman@19759
   162
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
huffman@19759
   163
done
huffman@19759
   164
huffman@19759
   165
lemma slen_fscons_less_eq:
hoelzl@43924
   166
        "(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))"
huffman@19759
   167
apply (subst slen_fscons_eq_rev)
huffman@19759
   168
apply (fast dest!: fscons_inject [THEN iffD1])
huffman@19759
   169
done
huffman@19759
   170
huffman@19759
   171
huffman@19759
   172
(* ------------------------------------------------------------------------- *)
huffman@19759
   173
huffman@19759
   174
section "induction"
huffman@19759
   175
huffman@19759
   176
lemma fstream_ind:
huffman@19759
   177
        "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x"
huffman@35781
   178
apply (erule stream.induct)
huffman@19759
   179
apply (assumption)
huffman@19759
   180
apply (unfold fscons_def2)
huffman@19759
   181
apply (fast dest: not_Undef_is_Def [THEN iffD1])
huffman@19759
   182
done
huffman@19759
   183
huffman@19759
   184
lemma fstream_ind2:
huffman@19759
   185
  "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x"
huffman@19759
   186
apply (erule stream_ind2)
huffman@19759
   187
apply (assumption)
huffman@19759
   188
apply (unfold fscons_def2)
huffman@19759
   189
apply (fast dest: not_Undef_is_Def [THEN iffD1])
huffman@19759
   190
apply (fast dest: not_Undef_is_Def [THEN iffD1])
huffman@19759
   191
done
huffman@19759
   192
huffman@19759
   193
huffman@19759
   194
(* ------------------------------------------------------------------------- *)
huffman@19759
   195
huffman@19759
   196
section "fsfilter"
huffman@19759
   197
huffman@19759
   198
lemma fsfilter_empty: "A(C)UU = UU"
huffman@19759
   199
apply (unfold fsfilter_def)
huffman@19759
   200
apply (rule sfilter_empty)
huffman@19759
   201
done
huffman@19759
   202
huffman@19759
   203
lemma fsfilter_fscons:
huffman@19759
   204
        "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)"
huffman@19759
   205
apply (unfold fsfilter_def)
huffman@35215
   206
apply (simp add: fscons_def2 If_and_if)
huffman@19759
   207
done
huffman@19759
   208
huffman@19759
   209
lemma fsfilter_emptys: "{}(C)x = UU"
huffman@19759
   210
apply (rule_tac x="x" in fstream_ind)
huffman@19759
   211
apply (simp)
huffman@19759
   212
apply (rule fsfilter_empty)
huffman@19759
   213
apply (simp add: fsfilter_fscons)
huffman@19759
   214
done
huffman@19759
   215
huffman@19759
   216
lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)"
huffman@19759
   217
by (simp add: fsfilter_fscons)
huffman@19759
   218
huffman@19759
   219
lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)"
huffman@19759
   220
by (rule fsfilter_insert)
huffman@19759
   221
huffman@19759
   222
lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)"
huffman@19759
   223
by (simp add: fsfilter_fscons)
huffman@19759
   224
huffman@19759
   225
lemma fstream_lub_lemma1:
huffman@27413
   226
    "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
huffman@19759
   227
apply (case_tac "max_in_chain i Y")
huffman@40771
   228
apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
huffman@19759
   229
apply  (force)
huffman@19759
   230
apply (unfold max_in_chain_def)
huffman@19759
   231
apply auto
huffman@25922
   232
apply (frule (1) chain_mono)
huffman@19759
   233
apply (rule_tac x="Y j" in fstream_cases)
huffman@19759
   234
apply  (force)
huffman@19759
   235
apply (drule_tac x="j" in is_ub_thelub)
huffman@19759
   236
apply (force)
huffman@19759
   237
done
huffman@19759
   238
huffman@19759
   239
lemma fstream_lub_lemma:
huffman@27413
   240
      "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) & (\<exists>X. chain X & (!i. ? j. Y j = a\<leadsto>X i) & (\<Squnion>i. X i) = s)"
huffman@19759
   241
apply (frule (1) fstream_lub_lemma1)
huffman@19759
   242
apply (clarsimp)
huffman@19759
   243
apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI)
huffman@19759
   244
apply (rule conjI)
huffman@19759
   245
apply  (erule chain_shift [THEN chain_monofun])
huffman@19759
   246
apply safe
huffman@25922
   247
apply  (drule_tac i="j" and j="i+j" in chain_mono)
huffman@19759
   248
apply   (simp)
huffman@19759
   249
apply  (simp)
huffman@19759
   250
apply  (rule_tac x="i+j" in exI)
huffman@19759
   251
apply  (drule fstream_prefix)
huffman@19759
   252
apply  (clarsimp)
huffman@41027
   253
apply  (subst lub_APP)
huffman@19759
   254
apply   (rule chainI)
huffman@19759
   255
apply   (fast)
huffman@19759
   256
apply  (erule chain_shift)
huffman@40771
   257
apply (subst lub_const)
huffman@19759
   258
apply (subst lub_range_shift)
huffman@19759
   259
apply  (assumption)
huffman@19759
   260
apply (simp)
huffman@19759
   261
done
huffman@19759
   262
oheimb@11350
   263
end