src/HOL/HOLCF/Library/Stream.thy
author immler
Sun, 27 Oct 2019 21:51:14 -0400
changeset 71035 6fe5a0e1fa8e
parent 67613 ce654b0e6d69
child 80914 d97fdabd9e2b
permissions -rw-r--r--
moved theory Interval from the AFP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41413
diff changeset
     1
(*  Title:      HOL/HOLCF/Library/Stream.thy
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
     2
    Author:     Franz Regensburger, David von Oheimb, Borislav Gajanovic
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     3
*)
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
     4
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 58880
diff changeset
     5
section \<open>General Stream domain\<close>
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
     6
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
     7
theory Stream
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 63549
diff changeset
     8
imports HOLCF "HOL-Library.Extended_Nat"
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
     9
begin
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    10
40329
73f2b99b549d change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents: 40327
diff changeset
    11
default_sort pcpo
73f2b99b549d change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents: 40327
diff changeset
    12
73f2b99b549d change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
huffman
parents: 40327
diff changeset
    13
domain (unsafe) 'a stream = scons (ft::'a) (lazy rt::"'a stream") (infixr "&&" 65)
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
    14
19763
wenzelm
parents: 19550
diff changeset
    15
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    16
  smap :: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream" where
19763
wenzelm
parents: 19550
diff changeset
    17
  "smap = fix\<cdot>(\<Lambda> h f s. case s of x && xs \<Rightarrow> f\<cdot>x && h\<cdot>f\<cdot>xs)"
11348
e08a0855af67 added stream length, map, and filter
oheimb
parents: 9169
diff changeset
    18
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    19
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    20
  sfilter :: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream" where
19763
wenzelm
parents: 19550
diff changeset
    21
  "sfilter = fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow>
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 40213
diff changeset
    22
                                     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs)"
11348
e08a0855af67 added stream length, map, and filter
oheimb
parents: 9169
diff changeset
    23
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    24
definition
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
    25
  slen :: "'a stream \<Rightarrow> enat"  ("#_" [1000] 1000) where
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
    26
  "#s = (if stream_finite s then enat (LEAST n. stream_take n\<cdot>s = s) else \<infinity>)"
19763
wenzelm
parents: 19550
diff changeset
    27
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    28
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    29
(* concatenation *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    30
19763
wenzelm
parents: 19550
diff changeset
    31
definition
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    32
  i_rt :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where (* chops the first i elements *)
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    33
  "i_rt = (\<lambda>i s. iterate i\<cdot>rt\<cdot>s)"
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
    34
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    35
definition
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    36
  i_th :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a" where (* the i-th element *)
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    37
  "i_th = (\<lambda>i s. ft\<cdot>(i_rt i s))"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    38
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 19763
diff changeset
    39
definition
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    40
  sconc :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream"  (infixr "ooo" 65) where
19763
wenzelm
parents: 19550
diff changeset
    41
  "s1 ooo s2 = (case #s1 of
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    42
                  enat n \<Rightarrow> (SOME s. (stream_take n\<cdot>s = s1) \<and> (i_rt n s = s2))
19763
wenzelm
parents: 19550
diff changeset
    43
               | \<infinity>     \<Rightarrow> s1)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    44
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    45
primrec constr_sconc' :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream"
27361
24ec32bee347 modernized specifications;
wenzelm
parents: 27111
diff changeset
    46
where
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    47
  constr_sconc'_0:   "constr_sconc' 0 s1 s2 = s2"
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    48
| constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft\<cdot>s1 && constr_sconc' n (rt\<cdot>s1) s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    49
19763
wenzelm
parents: 19550
diff changeset
    50
definition
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    51
  constr_sconc  :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where (* constructive *)
19763
wenzelm
parents: 19550
diff changeset
    52
  "constr_sconc s1 s2 = (case #s1 of
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
    53
                          enat n \<Rightarrow> constr_sconc' n s1 s2
19763
wenzelm
parents: 19550
diff changeset
    54
                        | \<infinity>    \<Rightarrow> s1)"
wenzelm
parents: 19550
diff changeset
    55
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    56
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    57
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    58
(* theorems about scons                                                    *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    59
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    60
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    61
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    62
section "scons"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    63
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    64
lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
30913
10b26965a08f domain package now generates iff rules for definedness of constructors
huffman
parents: 30807
diff changeset
    65
by simp
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    66
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    67
lemma scons_not_empty: "\<lbrakk>a && x = UU; a \<noteq> UU\<rbrakk> \<Longrightarrow> R"
30913
10b26965a08f domain package now generates iff rules for definedness of constructors
huffman
parents: 30807
diff changeset
    68
by simp
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    69
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    70
lemma stream_exhaust_eq: "x \<noteq> UU \<longleftrightarrow> (\<exists>a y. a \<noteq> UU \<and> x = a && y)"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
    71
by (cases x, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    72
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    73
lemma stream_neq_UU: "x \<noteq> UU \<Longrightarrow> \<exists>a a_s. x = a && a_s \<and> a \<noteq> UU"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    74
by (simp add: stream_exhaust_eq,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    75
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
    76
lemma stream_prefix:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    77
  "\<lbrakk>a && s \<sqsubseteq> t; a \<noteq> UU\<rbrakk> \<Longrightarrow> \<exists>b tt. t = b && tt \<and> b \<noteq> UU \<and> s \<sqsubseteq> tt"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
    78
by (cases t, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    79
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
    80
lemma stream_prefix':
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    81
  "b \<noteq> UU \<Longrightarrow> x \<sqsubseteq> b && z =
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    82
   (x = UU \<or> (\<exists>a y. x = a && y \<and> a \<noteq> UU \<and> a \<sqsubseteq> b \<and> y \<sqsubseteq> z))"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
    83
by (cases x, auto)
19550
ae77a20f6995 update to reflect changes in inverts/injects lemmas
huffman
parents: 19440
diff changeset
    84
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    85
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    86
(*
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    87
lemma stream_prefix1: "\<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys\<rbrakk> \<Longrightarrow> x && xs \<sqsubseteq> y && ys"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    88
by (insert stream_prefix' [of y "x && xs" ys],force)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    89
*)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    90
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
    91
lemma stream_flat_prefix:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    92
  "\<lbrakk>x && xs \<sqsubseteq> y && ys; (x::'a::flat) \<noteq> UU\<rbrakk> \<Longrightarrow> x = y \<and> xs \<sqsubseteq> ys"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
    93
apply (case_tac "y = UU",auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
    94
apply (drule ax_flat,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
    95
done
19550
ae77a20f6995 update to reflect changes in inverts/injects lemmas
huffman
parents: 19440
diff changeset
    96
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    97
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    98
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
    99
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   100
(* ----------------------------------------------------------------------- *)
40213
b63e966564da rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents: 40025
diff changeset
   101
(* theorems about stream_case                                              *)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   102
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   103
40213
b63e966564da rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents: 40025
diff changeset
   104
section "stream_case"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   105
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   106
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   107
lemma stream_case_strictf: "stream_case\<cdot>UU\<cdot>s = UU"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   108
by (cases s, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   109
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   110
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   111
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   112
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   113
(* theorems about ft and rt                                                *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   114
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   115
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   116
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   117
section "ft and rt"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   118
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   119
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   120
lemma ft_defin: "s \<noteq> UU \<Longrightarrow> ft\<cdot>s \<noteq> UU"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   121
by simp
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   122
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   123
lemma rt_strict_rev: "rt\<cdot>s \<noteq> UU \<Longrightarrow> s \<noteq> UU"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   124
by auto
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   125
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   126
lemma surjectiv_scons: "(ft\<cdot>s) && (rt\<cdot>s) = s"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   127
by (cases s, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   128
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   129
lemma monofun_rt_mult: "x \<sqsubseteq> s \<Longrightarrow> iterate i\<cdot>rt\<cdot>x \<sqsubseteq> iterate i\<cdot>rt\<cdot>s"
18075
43000d7a017c changed iterate to a continuous type
huffman
parents: 17291
diff changeset
   130
by (rule monofun_cfun_arg)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   131
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   132
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   133
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   134
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   135
(* theorems about stream_take                                              *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   136
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   137
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   138
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   139
section "stream_take"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   140
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   141
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   142
lemma stream_reach2: "(LUB i. stream_take i\<cdot>s) = s"
35494
45c9a8278faf domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents: 35444
diff changeset
   143
by (rule stream.reach)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   144
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   145
lemma chain_stream_take: "chain (\<lambda>i. stream_take i\<cdot>s)"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   146
by simp
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   147
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   148
lemma stream_take_prefix [simp]: "stream_take n\<cdot>s \<sqsubseteq> s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   149
apply (insert stream_reach2 [of s])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   150
apply (erule subst) back
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   151
apply (rule is_ub_thelub)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   152
apply (simp only: chain_stream_take)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   153
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   154
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   155
lemma stream_take_more [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   156
  "\<forall>x. stream_take n\<cdot>x = x \<longrightarrow> stream_take (Suc n)\<cdot>x = x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   157
apply (induct_tac n,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   158
apply (case_tac "x=UU",auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   159
apply (drule stream_exhaust_eq [THEN iffD1],auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   160
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   161
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   162
lemma stream_take_lemma3 [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   163
  "\<forall>x xs. x \<noteq> UU \<longrightarrow> stream_take n\<cdot>(x && xs) = x && xs \<longrightarrow> stream_take n\<cdot>xs = xs"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   164
apply (induct_tac n,clarsimp)
16745
5608017ee28b fixes to work with UU_reorient_simproc
huffman
parents: 16417
diff changeset
   165
(*apply (drule sym, erule scons_not_empty, simp)*)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   166
apply (clarify, rule stream_take_more)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   167
apply (erule_tac x="x" in allE)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   168
apply (erule_tac x="xs" in allE,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   169
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   170
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   171
lemma stream_take_lemma4:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   172
  "\<forall>x xs. stream_take n\<cdot>xs = xs \<longrightarrow> stream_take (Suc n)\<cdot>(x && xs) = x && xs"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   173
by auto
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   174
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   175
lemma stream_take_idempotent [rule_format, simp]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   176
  "\<forall>s. stream_take n\<cdot>(stream_take n\<cdot>s) = stream_take n\<cdot>s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   177
apply (induct_tac n, auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   178
apply (case_tac "s=UU", auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   179
apply (drule stream_exhaust_eq [THEN iffD1], auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   180
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   181
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   182
lemma stream_take_take_Suc [rule_format, simp]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   183
  "\<forall>s. stream_take n\<cdot>(stream_take (Suc n)\<cdot>s) = stream_take n\<cdot>s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   184
apply (induct_tac n, auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   185
apply (case_tac "s=UU", auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   186
apply (drule stream_exhaust_eq [THEN iffD1], auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   187
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   188
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   189
lemma mono_stream_take_pred:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   190
  "stream_take (Suc n)\<cdot>s1 \<sqsubseteq> stream_take (Suc n)\<cdot>s2 \<Longrightarrow>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   191
                       stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   192
by (insert monofun_cfun_arg [of "stream_take (Suc n)\<cdot>s1"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   193
  "stream_take (Suc n)\<cdot>s2" "stream_take n"], auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   194
(*
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   195
lemma mono_stream_take_pred:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   196
  "stream_take (Suc n)\<cdot>s1 \<sqsubseteq> stream_take (Suc n)\<cdot>s2 \<Longrightarrow>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   197
                       stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   198
by (drule mono_stream_take [of _ _ n],simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   199
*)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   200
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   201
lemma stream_take_lemma10 [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   202
  "\<forall>k\<le>n. stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2 \<longrightarrow> stream_take k\<cdot>s1 \<sqsubseteq> stream_take k\<cdot>s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   203
apply (induct_tac n,simp,clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   204
apply (case_tac "k=Suc n",blast)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   205
apply (erule_tac x="k" in allE)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   206
apply (drule mono_stream_take_pred,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   207
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   208
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   209
lemma stream_take_le_mono : "k \<le> n \<Longrightarrow> stream_take k\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s1"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   210
apply (insert chain_stream_take [of s1])
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   211
apply (drule chain_mono,auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   212
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   213
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   214
lemma mono_stream_take: "s1 \<sqsubseteq> s2 \<Longrightarrow> stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   215
by (simp add: monofun_cfun_arg)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   216
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   217
(*
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   218
lemma stream_take_prefix [simp]: "stream_take n\<cdot>s \<sqsubseteq> s"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   219
apply (subgoal_tac "s=(LUB n. stream_take n\<cdot>s)")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   220
 apply (erule ssubst, rule is_ub_thelub)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   221
 apply (simp only: chain_stream_take)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   222
by (simp only: stream_reach2)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   223
*)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   224
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   225
lemma stream_take_take_less:"stream_take k\<cdot>(stream_take n\<cdot>s) \<sqsubseteq> stream_take k\<cdot>s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   226
by (rule monofun_cfun_arg,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   227
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   228
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   229
(* ------------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   230
(* special induction rules                                                   *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   231
(* ------------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   232
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   233
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   234
section "induction"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   235
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   236
lemma stream_finite_ind:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   237
  "\<lbrakk>stream_finite x; P UU; \<And>a s. \<lbrakk>a \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (a && s)\<rbrakk> \<Longrightarrow> P x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   238
apply (simp add: stream.finite_def,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   239
apply (erule subst)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   240
apply (drule stream.finite_induct [of P _ x], auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   241
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   242
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   243
lemma stream_finite_ind2:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   244
  "\<lbrakk>P UU; \<And>x. x \<noteq> UU \<Longrightarrow> P (x && UU); \<And>y z s. \<lbrakk>y \<noteq> UU; z \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (y && z && s)\<rbrakk> \<Longrightarrow>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   245
                                 \<forall>s. P (stream_take n\<cdot>s)"
29855
e0ab6cf95539 Repaired a proof that did, after all, refer to the theorem nat_induct2.
paulson
parents: 29530
diff changeset
   246
apply (rule nat_less_induct [of _ n],auto)
e0ab6cf95539 Repaired a proof that did, after all, refer to the theorem nat_induct2.
paulson
parents: 29530
diff changeset
   247
apply (case_tac n, auto) 
e0ab6cf95539 Repaired a proof that did, after all, refer to the theorem nat_induct2.
paulson
parents: 29530
diff changeset
   248
apply (case_tac nat, auto) 
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   249
apply (case_tac "s=UU",clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   250
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   251
apply (case_tac "s=UU",clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   252
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   253
apply (case_tac "y=UU",clarsimp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   254
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   255
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   256
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   257
lemma stream_ind2:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   258
"\<lbrakk> adm P; P UU; \<And>a. a \<noteq> UU \<Longrightarrow> P (a && UU); \<And>a b s. \<lbrakk>a \<noteq> UU; b \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (a && b && s)\<rbrakk> \<Longrightarrow> P x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   259
apply (insert stream.reach [of x],erule subst)
35494
45c9a8278faf domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents: 35444
diff changeset
   260
apply (erule admD, rule chain_stream_take)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   261
apply (insert stream_finite_ind2 [of P])
35494
45c9a8278faf domain package no longer generates copy functions; all proofs use take functions instead
huffman
parents: 35444
diff changeset
   262
by simp
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   263
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   264
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   265
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   266
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   267
(* simplify use of coinduction                                             *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   268
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   269
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   270
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   271
section "coinduction"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   272
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   273
lemma stream_coind_lemma2: "\<forall>s1 s2. R s1 s2 \<longrightarrow> ft\<cdot>s1 = ft\<cdot>s2 \<and> R (rt\<cdot>s1) (rt\<cdot>s2) \<Longrightarrow> stream_bisim R"
30807
a167ed35ec0d domain package declares more simp rules
huffman
parents: 29855
diff changeset
   274
 apply (simp add: stream.bisim_def,clarsimp)
35497
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   275
 apply (drule spec, drule spec, drule (1) mp)
979706bd5c16 re-enable bisim code, now in domain_theorems.ML
huffman
parents: 35494
diff changeset
   276
 apply (case_tac "x", simp)
40025
876689e6bbdf reimplement proof automation for coinduct rules
huffman
parents: 40002
diff changeset
   277
 apply (case_tac "y", simp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   278
 apply auto
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   279
 done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   280
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   281
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   282
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   283
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   284
(* theorems about stream_finite                                            *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   285
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   286
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   287
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   288
section "stream_finite"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   289
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   290
lemma stream_finite_UU [simp]: "stream_finite UU"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   291
by (simp add: stream.finite_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   292
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   293
lemma stream_finite_UU_rev: "\<not> stream_finite s \<Longrightarrow> s \<noteq> UU"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   294
by (auto simp add: stream.finite_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   295
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   296
lemma stream_finite_lemma1: "stream_finite xs \<Longrightarrow> stream_finite (x && xs)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   297
apply (simp add: stream.finite_def,auto)
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35524
diff changeset
   298
apply (rule_tac x="Suc n" in exI)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   299
apply (simp add: stream_take_lemma4)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   300
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   301
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   302
lemma stream_finite_lemma2: "\<lbrakk>x \<noteq> UU; stream_finite (x && xs)\<rbrakk> \<Longrightarrow> stream_finite xs"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   303
apply (simp add: stream.finite_def, auto)
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35524
diff changeset
   304
apply (rule_tac x="n" in exI)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   305
apply (erule stream_take_lemma3,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   306
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   307
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   308
lemma stream_finite_rt_eq: "stream_finite (rt\<cdot>s) = stream_finite s"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   309
apply (cases s, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   310
apply (rule stream_finite_lemma1, simp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   311
apply (rule stream_finite_lemma2,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   312
apply assumption
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   313
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   314
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   315
lemma stream_finite_less: "stream_finite s \<Longrightarrow> \<forall>t. t \<sqsubseteq> s \<longrightarrow> stream_finite t"
19440
b2877e230b07 add lemma less_UU_iff as default simp rule
huffman
parents: 18109
diff changeset
   316
apply (erule stream_finite_ind [of s], auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   317
apply (case_tac "t=UU", auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   318
apply (drule stream_exhaust_eq [THEN iffD1],auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   319
apply (erule_tac x="y" in allE, simp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   320
apply (rule stream_finite_lemma1, simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   321
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   322
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   323
lemma stream_take_finite [simp]: "stream_finite (stream_take n\<cdot>s)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   324
apply (simp add: stream.finite_def)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   325
apply (rule_tac x="n" in exI,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   326
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   327
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   328
lemma adm_not_stream_finite: "adm (\<lambda>x. \<not> stream_finite x)"
25833
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   329
apply (rule adm_upward)
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   330
apply (erule contrapos_nn)
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   331
apply (erule (1) stream_finite_less [rule_format])
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   332
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   333
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   334
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   335
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   336
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   337
(* theorems about stream length                                            *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   338
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   339
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   340
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   341
section "slen"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   342
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   343
lemma slen_empty [simp]: "#\<bottom> = 0"
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   344
by (simp add: slen_def stream.finite_def zero_enat_def Least_equality)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   345
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   346
lemma slen_scons [simp]: "x \<noteq> \<bottom> \<Longrightarrow> #(x && xs) = eSuc (#xs)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   347
apply (case_tac "stream_finite (x && xs)")
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   348
apply (simp add: slen_def, auto)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   349
apply (simp add: stream.finite_def, auto simp add: eSuc_enat)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   350
apply (rule Least_Suc2, auto)
16745
5608017ee28b fixes to work with UU_reorient_simproc
huffman
parents: 16417
diff changeset
   351
(*apply (drule sym)*)
5608017ee28b fixes to work with UU_reorient_simproc
huffman
parents: 16417
diff changeset
   352
(*apply (drule sym scons_eq_UU [THEN iffD1],simp)*)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   353
apply (erule stream_finite_lemma2, simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   354
apply (simp add: slen_def, auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   355
apply (drule stream_finite_lemma1,auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   356
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   357
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
   358
lemma slen_less_1_eq: "(#x < enat (Suc 0)) = (x = \<bottom>)"
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   359
by (cases x) (auto simp add: enat_0 eSuc_enat[THEN sym])
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   360
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   361
lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   362
by (cases x) auto
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   363
67613
ce654b0e6d69 more symbols;
wenzelm
parents: 66453
diff changeset
   364
lemma slen_scons_eq: "(enat (Suc n) < #x) = (\<exists>a y. x = a && y \<and> a \<noteq> \<bottom> \<and> enat n < #y)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   365
apply (auto, case_tac "x=UU",auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   366
apply (drule stream_exhaust_eq [THEN iffD1], auto)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   367
apply (case_tac "#y") apply simp_all
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   368
apply (case_tac "#y") apply simp_all
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   369
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   370
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   371
lemma slen_eSuc: "#x = eSuc n \<longrightarrow> (\<exists>a y. x = a && y \<and> a \<noteq> \<bottom> \<and> #y = n)"
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   372
by (cases x) auto
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   373
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   374
lemma slen_stream_take_finite [simp]: "#(stream_take n\<cdot>s) \<noteq> \<infinity>"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   375
by (simp add: slen_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   376
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   377
lemma slen_scons_eq_rev: "#x < enat (Suc (Suc n)) \<longleftrightarrow> (\<forall>a y. x \<noteq> a && y \<or> a = \<bottom> \<or> #y < enat (Suc n))"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   378
 apply (cases x, auto)
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   379
   apply (simp add: zero_enat_def)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   380
  apply (case_tac "#stream") apply (simp_all add: eSuc_enat)
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   381
 apply (case_tac "#stream") apply (simp_all add: eSuc_enat)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   382
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   383
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   384
lemma slen_take_lemma4 [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   385
  "\<forall>s. stream_take n\<cdot>s \<noteq> s \<longrightarrow> #(stream_take n\<cdot>s) = enat n"
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
   386
apply (induct n, auto simp add: enat_0)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   387
apply (case_tac "s=UU", simp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   388
apply (drule stream_exhaust_eq [THEN iffD1], auto simp add: eSuc_enat)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   389
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   390
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   391
(*
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   392
lemma stream_take_idempotent [simp]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   393
 "stream_take n\<cdot>(stream_take n\<cdot>s) = stream_take n\<cdot>s"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   394
apply (case_tac "stream_take n\<cdot>s = s")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   395
apply (auto,insert slen_take_lemma4 [of n s]);
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   396
by (auto,insert slen_take_lemma1 [of "stream_take n\<cdot>s" n],simp)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   397
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   398
lemma stream_take_take_Suc [simp]: "stream_take n\<cdot>(stream_take (Suc n)\<cdot>s) =
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   399
                                    stream_take n\<cdot>s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   400
apply (simp add: po_eq_conv,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   401
 apply (simp add: stream_take_take_less)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   402
apply (subgoal_tac "stream_take n\<cdot>s = stream_take n\<cdot>(stream_take n\<cdot>s)")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   403
 apply (erule ssubst)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   404
 apply (rule_tac monofun_cfun_arg)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   405
 apply (insert chain_stream_take [of s])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   406
by (simp add: chain_def,simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   407
*)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   408
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   409
lemma slen_take_eq: "\<forall>x. enat n < #x \<longleftrightarrow> stream_take n\<cdot>x \<noteq> x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   410
apply (induct_tac n, auto)
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
   411
apply (simp add: enat_0, clarsimp)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   412
apply (drule not_sym)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   413
apply (drule slen_empty_eq [THEN iffD1], simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   414
apply (case_tac "x=UU", simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   415
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   416
apply (erule_tac x="y" in allE, auto)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   417
apply (simp_all add: not_less eSuc_enat)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   418
apply (case_tac "#y") apply simp_all
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   419
apply (case_tac "x=UU", simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   420
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   421
apply (erule_tac x="y" in allE, simp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   422
apply (case_tac "#y")
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   423
apply simp_all
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   424
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   425
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   426
lemma slen_take_eq_rev: "#x \<le> enat n \<longleftrightarrow> stream_take n\<cdot>x = x"
26102
2ae572207783 fix proofs involving ile_def
huffman
parents: 25922
diff changeset
   427
by (simp add: linorder_not_less [symmetric] slen_take_eq)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   428
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   429
lemma slen_take_lemma1: "#x = enat n \<Longrightarrow> stream_take n\<cdot>x = x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   430
by (rule slen_take_eq_rev [THEN iffD1], auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   431
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   432
lemma slen_rt_mono: "#s2 \<le> #s1 \<Longrightarrow> #(rt\<cdot>s2) \<le> #(rt\<cdot>s1)"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   433
apply (cases s1)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   434
 apply (cases s2, simp+)+
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   435
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   436
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   437
lemma slen_take_lemma5: "#(stream_take n\<cdot>s) \<le> enat n"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   438
apply (case_tac "stream_take n\<cdot>s = s")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   439
 apply (simp add: slen_take_eq_rev)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   440
apply (simp add: slen_take_lemma4)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   441
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   442
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   443
lemma slen_take_lemma2: "\<forall>x. \<not> stream_finite x \<longrightarrow> #(stream_take i\<cdot>x) = enat i"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   444
apply (simp add: stream.finite_def, auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   445
apply (simp add: slen_take_lemma4)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   446
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   447
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   448
lemma slen_infinite: "stream_finite x \<longleftrightarrow> #x \<noteq> \<infinity>"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   449
by (simp add: slen_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   450
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   451
lemma slen_mono_lemma: "stream_finite s \<Longrightarrow> \<forall>t. s \<sqsubseteq> t \<longrightarrow> #s \<le> #t"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   452
apply (erule stream_finite_ind [of s], auto)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   453
apply (case_tac "t = UU", auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   454
apply (drule stream_exhaust_eq [THEN iffD1], auto)
30807
a167ed35ec0d domain package declares more simp rules
huffman
parents: 29855
diff changeset
   455
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   456
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   457
lemma slen_mono: "s \<sqsubseteq> t \<Longrightarrow> #s \<le> #t"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   458
apply (case_tac "stream_finite t")
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   459
apply (frule stream_finite_less)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   460
apply (erule_tac x="s" in allE, simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   461
apply (drule slen_mono_lemma, auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   462
apply (simp add: slen_def)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   463
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   464
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   465
lemma iterate_lemma: "F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate n\<cdot>F\<cdot>(F\<cdot>x)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   466
by (insert iterate_Suc2 [of n F x], auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   467
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   468
lemma slen_rt_mult [rule_format]: "\<forall>x. enat (i + j) \<le> #x \<longrightarrow> enat j \<le> #(iterate i\<cdot>rt\<cdot>x)"
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   469
apply (induct i, auto)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   470
apply (case_tac "x = UU", auto simp add: zero_enat_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   471
apply (drule stream_exhaust_eq [THEN iffD1], auto)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   472
apply (erule_tac x = "y" in allE, auto)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   473
apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: eSuc_enat)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   474
apply (simp add: iterate_lemma)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   475
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   476
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   477
lemma slen_take_lemma3 [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   478
  "\<forall>(x::'a::flat stream) y. enat n \<le> #x \<longrightarrow> x \<sqsubseteq> y \<longrightarrow> stream_take n\<cdot>x = stream_take n\<cdot>y"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   479
apply (induct_tac n, auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   480
apply (case_tac "x=UU", auto)
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   481
apply (simp add: zero_enat_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   482
apply (simp add: Suc_ile_eq)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   483
apply (case_tac "y=UU", clarsimp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   484
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   485
apply (erule_tac x="ya" in allE, simp)
25920
8df5eabda5f6 change class axiom ax_flat to rule_format
huffman
parents: 25833
diff changeset
   486
by (drule ax_flat, simp)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   487
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   488
lemma slen_strict_mono_lemma:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   489
  "stream_finite t \<Longrightarrow> \<forall>s. #(s::'a::flat stream) = #t \<and> s \<sqsubseteq> t \<longrightarrow> s = t"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   490
apply (erule stream_finite_ind, auto)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   491
apply (case_tac "sa = UU", auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   492
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   493
apply (drule ax_flat, simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   494
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   495
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   496
lemma slen_strict_mono: "\<lbrakk>stream_finite t; s \<noteq> t; s \<sqsubseteq> (t::'a::flat stream)\<rbrakk> \<Longrightarrow> #s < #t"
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   497
by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   498
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   499
lemma stream_take_Suc_neq: "stream_take (Suc n)\<cdot>s \<noteq> s \<Longrightarrow>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   500
                     stream_take n\<cdot>s \<noteq> stream_take (Suc n)\<cdot>s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   501
apply auto
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   502
apply (subgoal_tac "stream_take n\<cdot>s \<noteq> s")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   503
 apply (insert slen_take_lemma4 [of n s],auto)
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   504
apply (cases s, simp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   505
apply (simp add: slen_take_lemma4 eSuc_enat)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   506
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   507
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   508
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   509
(* theorems about smap                                                     *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   510
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   511
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   512
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   513
section "smap"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   514
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   515
lemma smap_unfold: "smap = (\<Lambda> f t. case t of x && xs \<Rightarrow> f\<cdot>x && smap\<cdot>f\<cdot>xs)"
29530
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 27361
diff changeset
   516
by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   517
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   518
lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   519
by (subst smap_unfold, simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   520
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   521
lemma smap_scons [simp]: "x \<noteq> \<bottom> \<Longrightarrow> smap\<cdot>f\<cdot>(x && xs) = (f\<cdot>x) && (smap\<cdot>f\<cdot>xs)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   522
by (subst smap_unfold, force)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   523
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   524
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   525
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   526
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   527
(* theorems about sfilter                                                  *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   528
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   529
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   530
section "sfilter"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   531
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   532
lemma sfilter_unfold:
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   533
 "sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 40213
diff changeset
   534
  If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs)"
29530
9905b660612b change to simpler, more extensible continuity simproc
huffman
parents: 27361
diff changeset
   535
by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   536
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   537
lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
40002
c5b5f7a3a3b1 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents: 37110
diff changeset
   538
apply (rule cfun_eqI)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   539
apply (subst sfilter_unfold, auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   540
apply (case_tac "x=UU", auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   541
apply (drule stream_exhaust_eq [THEN iffD1], auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   542
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   543
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   544
lemma sfilter_empty [simp]: "sfilter\<cdot>f\<cdot>\<bottom> = \<bottom>"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   545
by (subst sfilter_unfold, force)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   546
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   547
lemma sfilter_scons [simp]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   548
  "x \<noteq> \<bottom> \<Longrightarrow> sfilter\<cdot>f\<cdot>(x && xs) =
40322
707eb30e8a53 make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents: 40213
diff changeset
   549
                           If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   550
by (subst sfilter_unfold, force)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   551
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   552
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   553
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   554
   section "i_rt"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   555
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   556
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   557
lemma i_rt_UU [simp]: "i_rt n UU = UU"
34941
156925dd67af dropped some old primrecs and some constdefs
haftmann
parents: 31084
diff changeset
   558
  by (induct n) (simp_all add: i_rt_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   559
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   560
lemma i_rt_0 [simp]: "i_rt 0 s = s"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   561
by (simp add: i_rt_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   562
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   563
lemma i_rt_Suc [simp]: "a \<noteq> UU \<Longrightarrow> i_rt (Suc n) (a&&s) = i_rt n s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   564
by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   565
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   566
lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt\<cdot>s)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   567
by (simp only: i_rt_def iterate_Suc2)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   568
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   569
lemma i_rt_Suc_back: "i_rt (Suc n) s = rt\<cdot>(i_rt n s)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   570
by (simp only: i_rt_def,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   571
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   572
lemma i_rt_mono: "x << s \<Longrightarrow> i_rt n x  << i_rt n s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   573
by (simp add: i_rt_def monofun_rt_mult)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   574
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   575
lemma i_rt_ij_lemma: "enat (i + j) \<le> #x \<Longrightarrow> enat j \<le> #(i_rt i x)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   576
by (simp add: i_rt_def slen_rt_mult)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   577
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   578
lemma slen_i_rt_mono: "#s2 \<le> #s1 \<Longrightarrow> #(i_rt n s2) \<le> #(i_rt n s1)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   579
apply (induct_tac n,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   580
apply (simp add: i_rt_Suc_back)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   581
apply (drule slen_rt_mono,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   582
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   583
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   584
lemma i_rt_take_lemma1 [rule_format]: "\<forall>s. i_rt n (stream_take n\<cdot>s) = UU"
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   585
apply (induct_tac n)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   586
 apply (simp add: i_rt_Suc_back,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   587
apply (case_tac "s=UU",auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   588
apply (drule stream_exhaust_eq [THEN iffD1],auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   589
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   590
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   591
lemma i_rt_slen: "i_rt n s = UU \<longleftrightarrow> stream_take n\<cdot>s = s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   592
apply auto
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   593
 apply (insert i_rt_ij_lemma [of n "Suc 0" s])
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   594
 apply (subgoal_tac "#(i_rt n s)=0")
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   595
  apply (case_tac "stream_take n\<cdot>s = s",simp+)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   596
  apply (insert slen_take_eq [rule_format,of n s],simp)
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   597
  apply (cases "#s") apply (simp_all add: zero_enat_def)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   598
  apply (simp add: slen_take_eq)
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   599
  apply (cases "#s")
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   600
  using i_rt_take_lemma1 [of n s]
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   601
  apply (simp_all add: zero_enat_def)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   602
  done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   603
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   604
lemma i_rt_lemma_slen: "#s=enat n \<Longrightarrow> i_rt n s = UU"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   605
by (simp add: i_rt_slen slen_take_lemma1)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   606
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   607
lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   608
apply (induct_tac n, auto)
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   609
 apply (cases s, auto simp del: i_rt_Suc)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   610
apply (simp add: i_rt_Suc_back stream_finite_rt_eq)+
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   611
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   612
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   613
lemma take_i_rt_len_lemma: "\<forall>sl x j t. enat sl = #x \<and> n \<le> sl \<and>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   614
                            #(stream_take n\<cdot>x) = enat t \<and> #(i_rt n x) = enat j
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   615
                                              \<longrightarrow> enat (j + t) = #x"
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   616
apply (induct n, auto)
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   617
 apply (simp add: zero_enat_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   618
apply (case_tac "x=UU",auto)
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   619
 apply (simp add: zero_enat_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   620
apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   621
apply (subgoal_tac "\<exists>k. enat k = #y",clarify)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   622
 apply (erule_tac x="k" in allE)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   623
 apply (erule_tac x="y" in allE,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   624
 apply (erule_tac x="THE p. Suc p = t" in allE,auto)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   625
   apply (simp add: eSuc_def split: enat.splits)
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   626
  apply (simp add: eSuc_def split: enat.splits)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   627
  apply (simp only: the_equality)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   628
 apply (simp add: eSuc_def split: enat.splits)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   629
 apply force
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   630
apply (simp add: eSuc_def split: enat.splits)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   631
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   632
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   633
lemma take_i_rt_len:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   634
"\<lbrakk>enat sl = #x; n \<le> sl; #(stream_take n\<cdot>x) = enat t; #(i_rt n x) = enat j\<rbrakk> \<Longrightarrow>
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
   635
    enat (j + t) = #x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   636
by (blast intro: take_i_rt_len_lemma [rule_format])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   637
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   638
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   639
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   640
   section "i_th"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   641
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   642
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   643
lemma i_th_i_rt_step:
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   644
"[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==>
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   645
   i_rt n s1 << i_rt n s2"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   646
apply (simp add: i_th_def i_rt_Suc_back)
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   647
apply (cases "i_rt n s1", simp)
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   648
apply (cases "i_rt n s2", auto)
30807
a167ed35ec0d domain package declares more simp rules
huffman
parents: 29855
diff changeset
   649
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   650
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   651
lemma i_th_stream_take_Suc [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   652
 "\<forall>s. i_th n (stream_take (Suc n)\<cdot>s) = i_th n s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   653
apply (induct_tac n,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   654
 apply (simp add: i_th_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   655
 apply (case_tac "s=UU",auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   656
 apply (drule stream_exhaust_eq [THEN iffD1],auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   657
apply (case_tac "s=UU",simp add: i_th_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   658
apply (drule stream_exhaust_eq [THEN iffD1],auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   659
apply (simp add: i_th_def i_rt_Suc_forw)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   660
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   661
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   662
lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)\<cdot>s)"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   663
apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)\<cdot>s)"])
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   664
apply (rule i_th_stream_take_Suc [THEN subst])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   665
apply (simp add: i_th_def  i_rt_Suc_back [symmetric])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   666
by (simp add: i_rt_take_lemma1)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   667
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   668
lemma i_th_last_eq:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   669
"i_th n s1 = i_th n s2 \<Longrightarrow> i_rt n (stream_take (Suc n)\<cdot>s1) = i_rt n (stream_take (Suc n)\<cdot>s2)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   670
apply (insert i_th_last [of n s1])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   671
apply (insert i_th_last [of n s2])
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   672
apply auto
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   673
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   674
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   675
lemma i_th_prefix_lemma:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   676
"\<lbrakk>k \<le> n; stream_take (Suc n)\<cdot>s1 << stream_take (Suc n)\<cdot>s2\<rbrakk> \<Longrightarrow>
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   677
    i_th k s1 << i_th k s2"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   678
apply (insert i_th_stream_take_Suc [of k s1, THEN sym])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   679
apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   680
apply (simp add: i_th_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   681
apply (rule monofun_cfun, auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   682
apply (rule i_rt_mono)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   683
apply (blast intro: stream_take_lemma10)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   684
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   685
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   686
lemma take_i_rt_prefix_lemma1:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   687
  "stream_take (Suc n)\<cdot>s1 << stream_take (Suc n)\<cdot>s2 \<Longrightarrow>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   688
   i_rt (Suc n) s1 << i_rt (Suc n) s2 \<Longrightarrow>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   689
   i_rt n s1 << i_rt n s2 \<and> stream_take n\<cdot>s1 << stream_take n\<cdot>s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   690
apply auto
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   691
 apply (insert i_th_prefix_lemma [of n n s1 s2])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   692
 apply (rule i_th_i_rt_step,auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   693
apply (drule mono_stream_take_pred,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   694
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   695
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   696
lemma take_i_rt_prefix_lemma:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   697
"\<lbrakk>stream_take n\<cdot>s1 << stream_take n\<cdot>s2; i_rt n s1 << i_rt n s2\<rbrakk> \<Longrightarrow> s1 << s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   698
apply (case_tac "n=0",simp)
25161
aa8474398030 changed back from ~=0 to >0
nipkow
parents: 22808
diff changeset
   699
apply (auto)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   700
apply (subgoal_tac "stream_take 0\<cdot>s1 << stream_take 0\<cdot>s2 \<and> i_rt 0 s1 << i_rt 0 s2")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   701
 defer 1
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   702
 apply (rule zero_induct,blast)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   703
 apply (blast dest: take_i_rt_prefix_lemma1)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   704
apply simp
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   705
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   706
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   707
lemma streams_prefix_lemma: "s1 << s2 \<longleftrightarrow>
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   708
  (stream_take n\<cdot>s1 << stream_take n\<cdot>s2 \<and> i_rt n s1 << i_rt n s2)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   709
apply auto
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   710
  apply (simp add: monofun_cfun_arg)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   711
 apply (simp add: i_rt_mono)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   712
apply (erule take_i_rt_prefix_lemma,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   713
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   714
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   715
lemma streams_prefix_lemma1:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   716
  "\<lbrakk>stream_take n\<cdot>s1 = stream_take n\<cdot>s2; i_rt n s1 = i_rt n s2\<rbrakk> \<Longrightarrow> s1 = s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   717
apply (simp add: po_eq_conv,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   718
 apply (insert streams_prefix_lemma)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   719
 apply blast+
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   720
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   721
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   722
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   723
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   724
   section "sconc"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   725
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   726
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   727
lemma UU_sconc [simp]: " UU ooo s = s "
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   728
by (simp add: sconc_def zero_enat_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   729
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   730
lemma scons_neq_UU: "a \<noteq> UU \<Longrightarrow> a && s \<noteq> UU"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   731
by auto
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   732
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   733
lemma singleton_sconc [rule_format, simp]: "x \<noteq> UU \<longrightarrow> (x && UU) ooo y = x && y"
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   734
apply (simp add: sconc_def zero_enat_def eSuc_def split: enat.splits, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   735
apply (rule someI2_ex,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   736
 apply (rule_tac x="x && y" in exI,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   737
apply (simp add: i_rt_Suc_forw)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   738
apply (case_tac "xa=UU",simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   739
by (drule stream_exhaust_eq [THEN iffD1],auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   740
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   741
lemma ex_sconc [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   742
  "\<forall>k y. #x = enat k \<longrightarrow> (\<exists>w. stream_take k\<cdot>w = x \<and> i_rt k w = y)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   743
apply (case_tac "#x")
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   744
 apply (rule stream_finite_ind [of x],auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   745
  apply (simp add: stream.finite_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   746
  apply (drule slen_take_lemma1,blast)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   747
 apply (simp_all add: zero_enat_def eSuc_def split: enat.splits)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   748
apply (erule_tac x="y" in allE,auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   749
apply (rule_tac x="a && w" in exI,auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   750
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   751
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   752
lemma rt_sconc1: "enat n = #x \<Longrightarrow> i_rt n (x ooo y) = y"
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
   753
apply (simp add: sconc_def split: enat.splits, arith?,auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   754
apply (rule someI2_ex,auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   755
apply (drule ex_sconc,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   756
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   757
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
   758
lemma sconc_inj2: "\<lbrakk>enat n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   759
apply (frule_tac y=y in rt_sconc1)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   760
apply (auto elim: rt_sconc1)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   761
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   762
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   763
lemma sconc_UU [simp]:"s ooo UU = s"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   764
apply (case_tac "#s")
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   765
 apply (simp add: sconc_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   766
 apply (rule someI2_ex)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   767
  apply (rule_tac x="s" in exI)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   768
  apply auto
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   769
   apply (drule slen_take_lemma1,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   770
  apply (simp add: i_rt_lemma_slen)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   771
 apply (drule slen_take_lemma1,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   772
 apply (simp add: i_rt_slen)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   773
apply (simp add: sconc_def)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   774
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   775
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   776
lemma stream_take_sconc [simp]: "enat n = #x \<Longrightarrow> stream_take n\<cdot>(x ooo y) = x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   777
apply (simp add: sconc_def)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   778
apply (cases "#x")
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   779
apply auto
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   780
apply (rule someI2_ex, auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   781
apply (drule ex_sconc,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   782
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   783
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   784
lemma scons_sconc [rule_format,simp]: "a \<noteq> UU \<longrightarrow> (a && x) ooo y = a && x ooo y"
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   785
apply (cases "#x",auto)
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   786
 apply (simp add: sconc_def eSuc_enat)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   787
 apply (rule someI2_ex)
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   788
  apply (drule ex_sconc, simp)
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   789
 apply (rule someI2_ex, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   790
  apply (simp add: i_rt_Suc_forw)
57492
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 49521
diff changeset
   791
  apply (rule_tac x="a && xa" in exI, auto)
74bf65a1910a Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents: 49521
diff changeset
   792
 apply (case_tac "xaa=UU",auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   793
 apply (drule stream_exhaust_eq [THEN iffD1],auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   794
 apply (drule streams_prefix_lemma1,simp+)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   795
apply (simp add: sconc_def)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   796
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   797
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   798
lemma ft_sconc: "x \<noteq> UU \<Longrightarrow> ft\<cdot>(x ooo y) = ft\<cdot>x"
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   799
by (cases x) auto
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   800
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   801
lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   802
apply (case_tac "#x")
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   803
 apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   804
  apply (simp add: stream.finite_def del: scons_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   805
  apply (drule slen_take_lemma1,auto simp del: scons_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   806
 apply (case_tac "a = UU", auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   807
by (simp add: sconc_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   808
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   809
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   810
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   811
25833
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   812
lemma cont_sconc_lemma1: "stream_finite x \<Longrightarrow> cont (\<lambda>y. x ooo y)"
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   813
by (erule stream_finite_ind, simp_all)
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   814
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   815
lemma cont_sconc_lemma2: "\<not> stream_finite x \<Longrightarrow> cont (\<lambda>y. x ooo y)"
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   816
by (simp add: sconc_def slen_def)
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   817
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   818
lemma cont_sconc: "cont (\<lambda>y. x ooo y)"
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   819
apply (cases "stream_finite x")
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   820
apply (erule cont_sconc_lemma1)
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   821
apply (erule cont_sconc_lemma2)
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   822
done
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   823
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   824
lemma sconc_mono: "y << y' \<Longrightarrow> x ooo y << x ooo y'"
25833
fe56cdb73ae5 simplified some proofs
huffman
parents: 25161
diff changeset
   825
by (rule cont_sconc [THEN cont2mono, THEN monofunE])
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   826
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   827
lemma sconc_mono1 [simp]: "x << x ooo y"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   828
by (rule sconc_mono [of UU, simplified])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   829
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   830
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   831
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   832
lemma empty_sconc [simp]: "x ooo y = UU \<longleftrightarrow> x = UU \<and> y = UU"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   833
apply (case_tac "#x",auto)
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   834
   apply (insert sconc_mono1 [of x y])
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   835
   apply auto
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   836
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   837
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   838
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   839
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   840
lemma rt_sconc [rule_format, simp]: "s \<noteq> UU \<longrightarrow> rt\<cdot>(s ooo x) = rt\<cdot>s ooo x"
35781
b7738ab762b1 renamed some lemmas generated by the domain package
huffman
parents: 35642
diff changeset
   841
by (cases s, auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   842
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   843
lemma i_th_sconc_lemma [rule_format]:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   844
  "\<forall>x y. enat n < #x \<longrightarrow> i_th n (x ooo y) = i_th n x"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   845
apply (induct_tac n, auto)
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
   846
apply (simp add: enat_0 i_th_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   847
apply (simp add: slen_empty_eq ft_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   848
apply (simp add: i_th_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   849
apply (case_tac "x=UU",auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   850
apply (drule stream_exhaust_eq [THEN iffD1], auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   851
apply (erule_tac x="ya" in allE)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   852
apply (case_tac "#ya")
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   853
apply simp_all
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   854
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   855
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   856
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   857
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   858
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   859
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   860
lemma sconc_lemma [rule_format, simp]: "\<forall>s. stream_take n\<cdot>s ooo i_rt n s = s"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   861
apply (induct_tac n,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   862
apply (case_tac "s=UU",auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   863
apply (drule stream_exhaust_eq [THEN iffD1],auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   864
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   865
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   866
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   867
   subsection "pointwise equality"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   868
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   869
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   870
lemma ex_last_stream_take_scons: "stream_take (Suc n)\<cdot>s =
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   871
                     stream_take n\<cdot>s ooo i_rt n (stream_take (Suc n)\<cdot>s)"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   872
by (insert sconc_lemma [of n "stream_take (Suc n)\<cdot>s"],simp)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   873
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   874
lemma i_th_stream_take_eq:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   875
  "\<And>n. \<forall>n. i_th n s1 = i_th n s2 \<Longrightarrow> stream_take n\<cdot>s1 = stream_take n\<cdot>s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   876
apply (induct_tac n,auto)
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   877
apply (subgoal_tac "stream_take (Suc na)\<cdot>s1 =
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   878
                    stream_take na\<cdot>s1 ooo i_rt na (stream_take (Suc na)\<cdot>s1)")
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   879
 apply (subgoal_tac "i_rt na (stream_take (Suc na)\<cdot>s1) =
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   880
                    i_rt na (stream_take (Suc na)\<cdot>s2)")
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   881
  apply (subgoal_tac "stream_take (Suc na)\<cdot>s2 =
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   882
                    stream_take na\<cdot>s2 ooo i_rt na (stream_take (Suc na)\<cdot>s2)")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   883
   apply (insert ex_last_stream_take_scons,simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   884
  apply blast
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   885
 apply (erule_tac x="na" in allE)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   886
 apply (insert i_th_last_eq [of _ s1 s2])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   887
by blast+
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   888
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   889
lemma pointwise_eq_lemma[rule_format]: "\<forall>n. i_th n s1 = i_th n s2 \<Longrightarrow> s1 = s2"
35642
f478d5a9d238 generate separate qualified theorem name for each type's reach and take_lemma
huffman
parents: 35557
diff changeset
   890
by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   891
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   892
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   893
   subsection "finiteness"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   894
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   895
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   896
lemma slen_sconc_finite1:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   897
  "\<lbrakk>#(x ooo y) = \<infinity>; enat n = #x\<rbrakk> \<Longrightarrow> #y = \<infinity>"
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   898
apply (case_tac "#y \<noteq> \<infinity>",auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   899
apply (drule_tac y=y in rt_sconc1)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   900
apply (insert stream_finite_i_rt [of n "x ooo y"])
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   901
apply (simp add: slen_infinite)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   902
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   903
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   904
lemma slen_sconc_infinite1: "#x=\<infinity> \<Longrightarrow> #(x ooo y) = \<infinity>"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   905
by (simp add: sconc_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   906
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   907
lemma slen_sconc_infinite2: "#y=\<infinity> \<Longrightarrow> #(x ooo y) = \<infinity>"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   908
apply (case_tac "#x")
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   909
 apply (simp add: sconc_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   910
 apply (rule someI2_ex)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   911
  apply (drule ex_sconc,auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   912
 apply (erule contrapos_pp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   913
 apply (insert stream_finite_i_rt)
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44019
diff changeset
   914
 apply (fastforce simp add: slen_infinite,auto)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   915
by (simp add: sconc_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   916
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   917
lemma sconc_finite: "#x \<noteq> \<infinity> \<and> #y \<noteq> \<infinity> \<longleftrightarrow> #(x ooo y) \<noteq> \<infinity>"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   918
apply auto
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   919
  apply (metis not_infinity_eq slen_sconc_finite1)
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   920
 apply (metis not_infinity_eq slen_sconc_infinite1)
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
   921
apply (metis not_infinity_eq slen_sconc_infinite2)
31084
f4db921165ce fixed HOLCF proofs
nipkow
parents: 30913
diff changeset
   922
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   923
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   924
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   925
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   926
lemma slen_sconc_mono3: "\<lbrakk>enat n = #x; enat k = #(x ooo y)\<rbrakk> \<Longrightarrow> n \<le> k"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   927
apply (insert slen_mono [of "x" "x ooo y"])
27111
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   928
apply (cases "#x") apply simp_all
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   929
apply (cases "#(x ooo y)") apply simp_all
c19be97e4553 adjusted some proofs involving inats
haftmann
parents: 26102
diff changeset
   930
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   931
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   932
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   933
   subsection "finite slen"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   934
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   935
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   936
lemma slen_sconc: "\<lbrakk>enat n = #x; enat m = #y\<rbrakk> \<Longrightarrow> #(x ooo y) = enat (n + m)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   937
apply (case_tac "#(x ooo y)")
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   938
 apply (frule_tac y=y in rt_sconc1)
43924
1165fe965da8 rename Fin to enat
hoelzl
parents: 43921
diff changeset
   939
 apply (insert take_i_rt_len [of "THE j. enat j = #(x ooo y)" "x ooo y" n n m],simp)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   940
 apply (insert slen_sconc_mono3 [of n x _ y],simp)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   941
apply (insert sconc_finite [of x y],auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   942
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   943
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   944
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   945
   subsection "flat prefix"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   946
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   947
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   948
lemma sconc_prefix: "(s1::'a::flat stream) << s2 \<Longrightarrow> \<exists>t. s1 ooo t = s2"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   949
apply (case_tac "#s1")
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   950
 apply (subgoal_tac "stream_take nat\<cdot>s1 = stream_take nat\<cdot>s2")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   951
  apply (rule_tac x="i_rt nat s2" in exI)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   952
  apply (simp add: sconc_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   953
  apply (rule someI2_ex)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   954
   apply (drule ex_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   955
   apply (simp,clarsimp,drule streams_prefix_lemma1)
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   956
   apply (simp+,rule slen_take_lemma3 [of _ s1 s2])
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   957
  apply (simp+,rule_tac x="UU" in exI)
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   958
apply (insert slen_take_lemma3 [of _ s1 s2])
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   959
apply (rule stream.take_lemma,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   960
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   961
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   962
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   963
   subsection "continuity"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   964
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   965
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   966
lemma chain_sconc: "chain S \<Longrightarrow> chain (\<lambda>i. (x ooo S i))"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   967
by (simp add: chain_def,auto simp add: sconc_mono)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   968
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   969
lemma chain_scons: "chain S \<Longrightarrow> chain (\<lambda>i. a && S i)"
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   970
apply (simp add: chain_def,auto)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   971
apply (rule monofun_cfun_arg,simp)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   972
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   973
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   974
lemma contlub_scons_lemma: "chain S \<Longrightarrow> (LUB i. a && S i) = a && (LUB i. S i)"
40327
1dfdbd66093a renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
huffman
parents: 40322
diff changeset
   975
by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric])
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   976
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   977
lemma finite_lub_sconc: "chain Y \<Longrightarrow> stream_finite x \<Longrightarrow>
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   978
                        (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   979
apply (rule stream_finite_ind [of x])
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   980
 apply (auto)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   981
apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)")
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   982
 apply (force,blast dest: contlub_scons_lemma chain_sconc)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
   983
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   984
17291
94f6113fe9ed converted to Isar theory format;
wenzelm
parents: 16745
diff changeset
   985
lemma contlub_sconc_lemma:
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   986
  "chain Y \<Longrightarrow> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
43921
e8511be08ddd Introduce infinity type class
hoelzl
parents: 43919
diff changeset
   987
apply (case_tac "#x=\<infinity>")
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   988
 apply (simp add: sconc_def)
18075
43000d7a017c changed iterate to a continuous type
huffman
parents: 17291
diff changeset
   989
apply (drule finite_lub_sconc,auto simp add: slen_infinite)
43000d7a017c changed iterate to a continuous type
huffman
parents: 17291
diff changeset
   990
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   991
63549
b0d31c7def86 more symbols;
wenzelm
parents: 62175
diff changeset
   992
lemma monofun_sconc: "monofun (\<lambda>y. x ooo y)"
16218
ea49a9c7ff7c fixed some renamed theorems
huffman
parents: 15188
diff changeset
   993
by (simp add: monofun_def sconc_mono)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   994
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   995
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   996
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   997
   section "constr_sconc"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   998
(* ----------------------------------------------------------------------- *)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
   999
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1000
lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s"
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 42151
diff changeset
  1001
by (simp add: constr_sconc_def zero_enat_def)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1002
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1003
lemma "x ooo y = constr_sconc x y"
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1004
apply (case_tac "#x")
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1005
 apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1006
  defer 1
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1007
  apply (simp add: constr_sconc_def del: scons_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1008
  apply (case_tac "#s")
44019
ee784502aed5 Extended_Nat.thy: renamed iSuc to eSuc, standardized theorem names
huffman
parents: 43924
diff changeset
  1009
   apply (simp add: eSuc_enat)
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1010
   apply (case_tac "a=UU",auto simp del: scons_sconc)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1011
   apply (simp)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1012
  apply (simp add: sconc_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1013
 apply (simp add: constr_sconc_def)
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1014
apply (simp add: stream.finite_def)
49521
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
  1015
apply (drule slen_take_lemma1,auto)
06cb12198b92 misc tuning;
wenzelm
parents: 44890
diff changeset
  1016
done
15188
9d57263faf9e integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
oheimb
parents: 14981
diff changeset
  1017
2570
24d7e8fb8261 added Classlib.* and Witness.*,
oheimb
parents:
diff changeset
  1018
end