wneuper/isa: src/HOL/HOLCF/IOA/meta_theory/Seq.thy@0437dbc127b3

     1 (*  Title:      HOLCF/IOA/meta_theory/Seq.thy

     2     Author:     Olaf Müller

     3 *)

     5 header {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}

     7 theory Seq

     8 imports HOLCF

     9 begin

    11 default_sort pcpo

    13 domain (unsafe) 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)

    15 (*

    16    sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"

    17    smap          :: "('a -> 'b) -> 'a seq -> 'b seq"

    18    sforall       :: "('a -> tr) => 'a seq => bool"

    19    sforall2      :: "('a -> tr) -> 'a seq -> tr"

    20    slast         :: "'a seq     -> 'a"

    21    sconc         :: "'a seq     -> 'a seq -> 'a seq"

    22    sdropwhile    :: "('a -> tr)  -> 'a seq -> 'a seq"

    23    stakewhile    :: "('a -> tr)  -> 'a seq -> 'a seq"

    24    szip          :: "'a seq      -> 'b seq -> ('a*'b) seq"

    25    sflat        :: "('a seq) seq  -> 'a seq"

    27    sfinite       :: "'a seq set"

    28    Partial       :: "'a seq => bool"

    29    Infinite      :: "'a seq => bool"

    31    nproj        :: "nat => 'a seq => 'a"

    32    sproj        :: "nat => 'a seq => 'a seq"

    33 *)

    35 inductive

    36   Finite :: "'a seq => bool"

    37   where

    38     sfinite_0:  "Finite nil"

    39   | sfinite_n:  "[| Finite tr; a~=UU |] ==> Finite (a##tr)"

    41 declare Finite.intros [simp]

    43 definition

    44   Partial :: "'a seq => bool"

    45 where

    46   "Partial x  == (seq_finite x) & ~(Finite x)"

    48 definition

    49   Infinite :: "'a seq => bool"

    50 where

    51   "Infinite x == ~(seq_finite x)"

    54 subsection {* recursive equations of operators *}

    56 subsubsection {* smap *}

    58 fixrec

    59   smap :: "('a -> 'b) -> 'a seq -> 'b seq"

    60 where

    61   smap_nil: "smap$f$nil=nil"

    62 | smap_cons: "[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"

    64 lemma smap_UU [simp]: "smap$f$UU=UU"

    65 by fixrec_simp

    67 subsubsection {* sfilter *}

    69 fixrec

    70    sfilter :: "('a -> tr) -> 'a seq -> 'a seq"

    71 where

    72   sfilter_nil: "sfilter$P$nil=nil"

    73 | sfilter_cons:

    74     "x~=UU ==> sfilter$P$(x##xs)=

    75               (If P$x then x##(sfilter$P$xs) else sfilter$P$xs)"

    77 lemma sfilter_UU [simp]: "sfilter$P$UU=UU"

    78 by fixrec_simp

    80 subsubsection {* sforall2 *}

    82 fixrec

    83   sforall2 :: "('a -> tr) -> 'a seq -> tr"

    84 where

    85   sforall2_nil: "sforall2$P$nil=TT"

    86 | sforall2_cons:

    87     "x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)"

    89 lemma sforall2_UU [simp]: "sforall2$P$UU=UU"

    90 by fixrec_simp

    92 definition

    93   sforall_def: "sforall P t == (sforall2$P$t ~=FF)"

    95 subsubsection {* stakewhile *}

    97 fixrec

    98   stakewhile :: "('a -> tr)  -> 'a seq -> 'a seq"

    99 where

   100   stakewhile_nil: "stakewhile$P$nil=nil"

   101 | stakewhile_cons:

   102     "x~=UU ==> stakewhile$P$(x##xs) =

   103               (If P$x then x##(stakewhile$P$xs) else nil)"

   105 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"

   106 by fixrec_simp

   108 subsubsection {* sdropwhile *}

   110 fixrec

   111   sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"

   112 where

   113   sdropwhile_nil: "sdropwhile$P$nil=nil"

   114 | sdropwhile_cons:

   115     "x~=UU ==> sdropwhile$P$(x##xs) =

   116               (If P$x then sdropwhile$P$xs else x##xs)"

   118 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"

   119 by fixrec_simp

   121 subsubsection {* slast *}

   123 fixrec

   124   slast :: "'a seq -> 'a"

   125 where

   126   slast_nil: "slast$nil=UU"

   127 | slast_cons:

   128     "x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs)"

   130 lemma slast_UU [simp]: "slast$UU=UU"

   131 by fixrec_simp

   133 subsubsection {* sconc *}

   135 fixrec

   136   sconc :: "'a seq -> 'a seq -> 'a seq"

   137 where

   138   sconc_nil: "sconc$nil$y = y"

   139 | sconc_cons':

   140     "x~=UU ==> sconc$(x##xs)$y = x##(sconc$xs$y)"

   142 abbreviation

   143   sconc_syn :: "'a seq => 'a seq => 'a seq"  (infixr "@@" 65) where

   144   "xs @@ ys == sconc $ xs $ ys"

   146 lemma sconc_UU [simp]: "UU @@ y=UU"

   147 by fixrec_simp

   149 lemma sconc_cons [simp]: "(x##xs) @@ y=x##(xs @@ y)"

   150 apply (cases "x=UU")

   151 apply simp_all

   152 done

   154 declare sconc_cons' [simp del]

   156 subsubsection {* sflat *}

   158 fixrec

   159   sflat :: "('a seq) seq -> 'a seq"

   160 where

   161   sflat_nil: "sflat$nil=nil"

   162 | sflat_cons': "x~=UU ==> sflat$(x##xs)= x@@(sflat$xs)"

   164 lemma sflat_UU [simp]: "sflat$UU=UU"

   165 by fixrec_simp

   167 lemma sflat_cons [simp]: "sflat$(x##xs)= x@@(sflat$xs)"

   168 by (cases "x=UU", simp_all)

   170 declare sflat_cons' [simp del]

   172 subsubsection {* szip *}

   174 fixrec

   175   szip :: "'a seq -> 'b seq -> ('a*'b) seq"

   176 where

   177   szip_nil: "szip$nil$y=nil"

   178 | szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU"

   179 | szip_cons:

   180     "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = (x,y)##szip$xs$ys"

   182 lemma szip_UU1 [simp]: "szip$UU$y=UU"

   183 by fixrec_simp

   185 lemma szip_UU2 [simp]: "x~=nil ==> szip$x$UU=UU"

   186 by (cases x, simp_all, fixrec_simp)

   189 subsection "scons, nil"

   191 lemma scons_inject_eq:

   192  "[|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"

   193 by simp

   195 lemma nil_less_is_nil: "nil<<x ==> nil=x"

   196 apply (cases x)

   197 apply simp

   198 apply simp

   199 apply simp

   200 done

   202 subsection "sfilter, sforall, sconc"

   204 lemma if_and_sconc [simp]: "(if b then tr1 else tr2) @@ tr

   205         = (if b then tr1 @@ tr else tr2 @@ tr)"

   206 by simp

   209 lemma sfiltersconc: "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)"

   210 apply (induct x)

   211 (* adm *)

   212 apply simp

   213 (* base cases *)

   214 apply simp

   215 apply simp

   216 (* main case *)

   217 apply (rule_tac p="P$a" in trE)

   218 apply simp

   219 apply simp

   220 apply simp

   221 done

   223 lemma sforallPstakewhileP: "sforall P (stakewhile$P$x)"

   224 apply (simp add: sforall_def)

   225 apply (induct x)

   226 (* adm *)

   227 apply simp

   228 (* base cases *)

   229 apply simp

   230 apply simp

   231 (* main case *)

   232 apply (rule_tac p="P$a" in trE)

   233 apply simp

   234 apply simp

   235 apply simp

   236 done

   238 lemma forallPsfilterP: "sforall P (sfilter$P$x)"

   239 apply (simp add: sforall_def)

   240 apply (induct x)

   241 (* adm *)

   242 apply simp

   243 (* base cases *)

   244 apply simp

   245 apply simp

   246 (* main case *)

   247 apply (rule_tac p="P$a" in trE)

   248 apply simp

   249 apply simp

   250 apply simp

   251 done

   254 subsection "Finite"

   256 (* ----------------------------------------------------  *)

   257 (* Proofs of rewrite rules for Finite:                  *)

   258 (* 1. Finite(nil),   (by definition)                    *)

   259 (* 2. ~Finite(UU),                                      *)

   260 (* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)

   261 (* ----------------------------------------------------  *)

   263 lemma Finite_UU_a: "Finite x --> x~=UU"

   264 apply (rule impI)

   265 apply (erule Finite.induct)

   266  apply simp

   267 apply simp

   268 done

   270 lemma Finite_UU [simp]: "~(Finite UU)"

   271 apply (cut_tac x="UU" in Finite_UU_a)

   272 apply fast

   273 done

   275 lemma Finite_cons_a: "Finite x --> a~=UU --> x=a##xs --> Finite xs"

   276 apply (intro strip)

   277 apply (erule Finite.cases)

   278 apply fastsimp

   279 apply simp

   280 done

   282 lemma Finite_cons: "a~=UU ==>(Finite (a##x)) = (Finite x)"

   283 apply (rule iffI)

   284 apply (erule (1) Finite_cons_a [rule_format])

   285 apply fast

   286 apply simp

   287 done

   289 lemma Finite_upward: "\<lbrakk>Finite x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> Finite y"

   290 apply (induct arbitrary: y set: Finite)

   291 apply (case_tac y, simp, simp, simp)

   292 apply (case_tac y, simp, simp)

   293 apply simp

   294 done

   296 lemma adm_Finite [simp]: "adm Finite"

   297 by (rule adm_upward, rule Finite_upward)

   300 subsection "induction"

   303 (*--------------------------------   *)

   304 (* Extensions to Induction Theorems  *)

   305 (*--------------------------------   *)

   308 lemma seq_finite_ind_lemma:

   309   assumes "(!!n. P(seq_take n$s))"

   310   shows "seq_finite(s) -->P(s)"

   311 apply (unfold seq.finite_def)

   312 apply (intro strip)

   313 apply (erule exE)

   314 apply (erule subst)

   315 apply (rule prems)

   316 done

   319 lemma seq_finite_ind: "!!P.[|P(UU);P(nil);

   320    !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)

   321    |] ==> seq_finite(s) --> P(s)"

   322 apply (rule seq_finite_ind_lemma)

   323 apply (erule seq.finite_induct)

   324  apply assumption

   325 apply simp

   326 done

   328 end

author	huffman
	Sat, 27 Nov 2010 16:08:10 -0800
changeset 41022	0437dbc127b3
parent 40567	src/HOLCF/IOA/meta_theory/Seq.thy@73f2b99b549d
child 41193	b8703f63bfb2
permissions	-rw-r--r--