src/HOL/HOLCF/FOCUS/Fstream.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45049 13efaee97111
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41476
diff changeset
     1
(*  Title:      HOL/HOLCF/FOCUS/Fstream.thy
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15188
diff changeset
     2
    Author:     David von Oheimb, TU Muenchen
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     3
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30807
diff changeset
     4
FOCUS streams (with lifted elements).
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30807
diff changeset
     5
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30807
diff changeset
     6
TODO: integrate Fstreams.thy
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     7
*)
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
     8
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15188
diff changeset
     9
header {* FOCUS flat streams *}
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    10
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15188
diff changeset
    11
theory Fstream
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 41027
diff changeset
    12
imports "~~/src/HOL/HOLCF/Library/Stream"
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15188
diff changeset
    13
begin
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    14
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35781
diff changeset
    15
default_sort type
17293
ecf182ccc3ca converted to Isar theory format;
wenzelm
parents: 15188
diff changeset
    16
41476
0fa9629aa399 types -> type_synonym
huffman
parents: 41413
diff changeset
    17
type_synonym 'a fstream = "'a lift stream"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    18
19763
wenzelm
parents: 19759
diff changeset
    19
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    20
  fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
19763
wenzelm
parents: 19759
diff changeset
    21
  "fscons a = (\<Lambda> s. Def a && s)"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    22
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    23
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    24
  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
19763
wenzelm
parents: 19759
diff changeset
    25
  "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    26
19763
wenzelm
parents: 19759
diff changeset
    27
abbreviation
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    28
  emptystream   :: "'a fstream"                          ("<>") where
19763
wenzelm
parents: 19759
diff changeset
    29
  "<> == \<bottom>"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    30
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    31
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    32
  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_~>_)"    [66,65] 65) where
19763
wenzelm
parents: 19759
diff changeset
    33
  "a~>s == fscons a\<cdot>s"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    34
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    35
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    36
  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_'(C')_)" [64,63] 63) where
19763
wenzelm
parents: 19759
diff changeset
    37
  "A(C)s == fsfilter A\<cdot>s"
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    38
21210
c17fd2df4e9e renamed 'const_syntax' to 'notation';
wenzelm
parents: 19764
diff changeset
    39
notation (xsymbols)
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    40
  fscons'  ("(_\<leadsto>_)"                                                 [66,65] 65) and
19763
wenzelm
parents: 19759
diff changeset
    41
  fsfilter'  ("(_\<copyright>_)"                                               [64,63] 63)
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    42
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
    43
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    44
lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
40087
1b5f394866d9 simplify proof
huffman
parents: 40009
diff changeset
    45
by simp
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    46
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    47
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    48
section "fscons"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    49
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    50
lemma fscons_def2: "a~>s = Def a && s"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    51
apply (unfold fscons_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    52
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    53
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    54
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    55
lemma fstream_exhaust: "x = UU |  (? a y. x = a~> y)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    56
apply (simp add: fscons_def2)
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35532
diff changeset
    57
apply (cut_tac stream.nchotomy)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    58
apply (fast dest: not_Undef_is_Def [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    59
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    60
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    61
lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    62
apply (cut_tac fstream_exhaust)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    63
apply (erule disjE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    64
apply fast
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    65
apply fast
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    66
done
27148
5b78e50adc49 removed dead code;
wenzelm
parents: 25922
diff changeset
    67
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    68
lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    69
apply (simp add: fscons_def2 stream_exhaust_eq)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    70
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    71
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    72
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    73
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    74
lemma fscons_not_empty [simp]: "a~> s ~= <>"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    75
by (simp add: fscons_def2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    76
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    77
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    78
lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b &  s = t)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    79
by (simp add: fscons_def2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    80
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    81
lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt &  s << tt"
35532
60647586b173 adapt to changed variable name in casedist theorem
huffman
parents: 35215
diff changeset
    82
apply (cases t)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    83
apply (cut_tac fscons_not_empty)
45049
13efaee97111 discontinued HOLCF legacy theorem names
huffman
parents: 44019
diff changeset
    84
apply (fast dest: bottomI)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    85
apply (simp add: fscons_def2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    86
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    87
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    88
lemma fstream_prefix' [simp]:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    89
        "x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))"
45049
13efaee97111 discontinued HOLCF legacy theorem names
huffman
parents: 44019
diff changeset
    90
apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix'])
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    91
apply (safe)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    92
apply (erule_tac [!] contrapos_np)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    93
prefer 2 apply (fast elim: DefE)
40009
f2c78550c0b7 remove unneeded lemmas Lift_exhaust, Lift_cases
huffman
parents: 39159
diff changeset
    94
apply (rule lift.exhaust)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    95
apply (erule (1) notE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    96
apply (safe)
40431
682d6c455670 discontinue a bunch of legacy theorem names
huffman
parents: 40087
diff changeset
    97
apply (drule Def_below_Def [THEN iffD1])
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    98
apply fast
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
    99
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   100
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   101
(* ------------------------------------------------------------------------- *)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   102
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   103
section "ft & rt"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   104
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   105
lemmas ft_empty = stream.sel_rews (1)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   106
lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   107
by (simp add: fscons_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   108
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   109
lemmas rt_empty = stream.sel_rews (2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   110
lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   111
by (simp add: fscons_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   112
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   113
lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (? t. s = a~> t)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   114
apply (unfold fscons_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   115
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   116
apply (safe)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   117
apply (erule subst)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   118
apply (rule exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   119
apply (rule surjectiv_scons [symmetric])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   120
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   121
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   122
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   123
lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   124
by auto
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   125
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   126
lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   127
by (simp add: surjective_fscons_lemma)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   128
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   129
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   130
(* ------------------------------------------------------------------------- *)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   131
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   132
section "take"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   133
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   134
lemma fstream_take_Suc [simp]:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   135
        "stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   136
by (simp add: fscons_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   137
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   138
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   139
(* ------------------------------------------------------------------------- *)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   140
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   141
section "slen"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   142
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   143
lemma slen_fscons: "#(m~> s) = eSuc (#s)"
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   144
by (simp add: fscons_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   145
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   146
lemma slen_fscons_eq:
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42793
diff changeset
   147
        "(enat (Suc n) < #x) = (? a y. x = a~> y & enat n < #y)"
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   148
apply (simp add: fscons_def2 slen_scons_eq)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   149
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   150
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   151
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   152
lemma slen_fscons_eq_rev:
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42793
diff changeset
   153
        "(#x < enat (Suc (Suc n))) = (!a y. x ~= a~> y | #y < enat (Suc n))"
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   154
apply (simp add: fscons_def2 slen_scons_eq_rev)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42151
diff changeset
   155
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42151
diff changeset
   156
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42151
diff changeset
   157
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42151
diff changeset
   158
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42151
diff changeset
   159
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42151
diff changeset
   160
apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   161
apply (erule contrapos_np)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   162
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   163
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   164
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   165
lemma slen_fscons_less_eq:
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 42793
diff changeset
   166
        "(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))"
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   167
apply (subst slen_fscons_eq_rev)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   168
apply (fast dest!: fscons_inject [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   169
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   170
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   171
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   172
(* ------------------------------------------------------------------------- *)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   173
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   174
section "induction"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   175
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   176
lemma fstream_ind:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   177
        "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35532
diff changeset
   178
apply (erule stream.induct)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   179
apply (assumption)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   180
apply (unfold fscons_def2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   181
apply (fast dest: not_Undef_is_Def [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   182
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   183
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   184
lemma fstream_ind2:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   185
  "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   186
apply (erule stream_ind2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   187
apply (assumption)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   188
apply (unfold fscons_def2)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   189
apply (fast dest: not_Undef_is_Def [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   190
apply (fast dest: not_Undef_is_Def [THEN iffD1])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   191
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   192
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   193
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   194
(* ------------------------------------------------------------------------- *)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   195
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   196
section "fsfilter"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   197
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   198
lemma fsfilter_empty: "A(C)UU = UU"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   199
apply (unfold fsfilter_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   200
apply (rule sfilter_empty)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   201
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   202
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   203
lemma fsfilter_fscons:
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   204
        "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   205
apply (unfold fsfilter_def)
35215
a03462cbf86f get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents: 32960
diff changeset
   206
apply (simp add: fscons_def2 If_and_if)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   207
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   208
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   209
lemma fsfilter_emptys: "{}(C)x = UU"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   210
apply (rule_tac x="x" in fstream_ind)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   211
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   212
apply (rule fsfilter_empty)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   213
apply (simp add: fsfilter_fscons)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   214
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   215
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   216
lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   217
by (simp add: fsfilter_fscons)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   218
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   219
lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   220
by (rule fsfilter_insert)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   221
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   222
lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)"
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   223
by (simp add: fsfilter_fscons)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   224
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   225
lemma fstream_lub_lemma1:
27413
3154f3765cc7 replace lub (range Y) with (LUB i. Y i)
huffman
parents: 27148
diff changeset
   226
    "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   227
apply (case_tac "max_in_chain i Y")
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40431
diff changeset
   228
apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   229
apply  (force)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   230
apply (unfold max_in_chain_def)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   231
apply auto
25922
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 24327
diff changeset
   232
apply (frule (1) chain_mono)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   233
apply (rule_tac x="Y j" in fstream_cases)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   234
apply  (force)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   235
apply (drule_tac x="j" in is_ub_thelub)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   236
apply (force)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   237
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   238
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   239
lemma fstream_lub_lemma:
27413
3154f3765cc7 replace lub (range Y) with (LUB i. Y i)
huffman
parents: 27148
diff changeset
   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)"
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   241
apply (frule (1) fstream_lub_lemma1)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   242
apply (clarsimp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   243
apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   244
apply (rule conjI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   245
apply  (erule chain_shift [THEN chain_monofun])
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   246
apply safe
25922
cb04d05e95fb rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents: 24327
diff changeset
   247
apply  (drule_tac i="j" and j="i+j" in chain_mono)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   248
apply   (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   249
apply  (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   250
apply  (rule_tac x="i+j" in exI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   251
apply  (drule fstream_prefix)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   252
apply  (clarsimp)
41027
c599955d9806 add lemmas lub_APP, lub_LAM
huffman
parents: 40774
diff changeset
   253
apply  (subst lub_APP)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   254
apply   (rule chainI)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   255
apply   (fast)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   256
apply  (erule chain_shift)
40771
1c6f7d4b110e renamed several HOLCF theorems (listed in NEWS)
huffman
parents: 40431
diff changeset
   257
apply (subst lub_const)
19759
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   258
apply (subst lub_range_shift)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   259
apply  (assumption)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   260
apply (simp)
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   261
done
2d0896653e7a removed legacy ML scripts
huffman
parents: 17293
diff changeset
   262
11350
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy
oheimb
parents:
diff changeset
   263
end