Quelle  Seq.thy   Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/Seq.thy
    Author:     Olaf Müller
*)

section ‹Partial, Finite and Infinite Sequences (lazy lists), modeled as domain›

theory Seq
imports HOLCF
begin

default_sort pcpo

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

inductive Finite :: "'a seq \ bool"
where
  sfinite_0: "Finite nil"
| sfinite_n: "Finite tr \ a \ UU \ Finite (a ## tr)"

declare Finite.intros [simp]

definition Partial :: "'a seq \ bool"
  where "Partial x \ seq_finite x \ \ Finite x"

definition Infinite :: "'a seq \ bool"
  where "Infinite x \ \ seq_finite x"


subsection ‹Recursive equations of operators›

subsubsection ‹‹smap››

fixrec smap :: "('a \ 'b) \ 'a seq \ 'b seq"
where
  smap_nil: "smap \ f \ nil = nil"
| smap_cons: "x \ UU \ smap \ f \ (x ## xs) = (f \ x) ## smap \ f \ xs"

lemma smap_UU [simp]: "smap \ f \ UU = UU"
  by fixrec_simp


subsubsection ‹‹sfilter››

fixrec sfilter :: "('a \ tr) \ 'a seq \ 'a seq"
where
  sfilter_nil: "sfilter \ P \ nil = nil"
| sfilter_cons:
    "x \ UU \
      sfilter ⋅ P ⋅ (x ## xs) =
      (If P ⋅ x then x ## (sfilter ⋅ P ⋅ xs) else sfilter ⋅ P ⋅ xs)"

lemma sfilter_UU [simp]: "sfilter \ P \ UU = UU"
  by fixrec_simp


subsubsection ‹‹sforall2››

fixrec sforall2 :: "('a \ tr) \ 'a seq \ tr"
where
  sforall2_nil: "sforall2 \ P \ nil = TT"
| sforall2_cons: "x \ UU \ sforall2 \ P \ (x ## xs) = ((P \ x) andalso sforall2 \ P \ xs)"

lemma sforall2_UU [simp]: "sforall2 \ P \ UU = UU"
  by fixrec_simp

definition "sforall P t \ sforall2 \ P \ t \ FF"


subsubsection ‹‹stakewhile››

fixrec stakewhile :: "('a \ tr) \ 'a seq \ 'a seq"
where
  stakewhile_nil: "stakewhile \ P \ nil = nil"
| stakewhile_cons:
    "x \ UU \ stakewhile \ P \ (x ## xs) = (If P \ x then x ## (stakewhile \ P \ xs) else nil)"

lemma stakewhile_UU [simp]: "stakewhile \ P \ UU = UU"
  by fixrec_simp


subsubsection ‹‹sdropwhile››

fixrec sdropwhile :: "('a \ tr) \ 'a seq \ 'a seq"
where
  sdropwhile_nil: "sdropwhile \ P \ nil = nil"
| sdropwhile_cons:
    "x \ UU \ sdropwhile \ P \ (x ## xs) = (If P \ x then sdropwhile \ P \ xs else x ## xs)"

lemma sdropwhile_UU [simp]: "sdropwhile \ P \ UU = UU"
  by fixrec_simp


subsubsection ‹‹slast››

fixrec slast :: "'a seq \ 'a"
where
  slast_nil: "slast \ nil = UU"
| slast_cons: "x \ UU \ slast \ (x ## xs) = (If is_nil \ xs then x else slast \ xs)"

lemma slast_UU [simp]: "slast \ UU = UU"
  by fixrec_simp


subsubsection ‹‹sconc››

fixrec sconc :: "'a seq \ 'a seq \ 'a seq"
where
  sconc_nil: "sconc \ nil \ y = y"
| sconc_cons': "x \ UU \ sconc \ (x ## xs) \ y = x ## (sconc \ xs \ y)"

abbreviation sconc_syn :: "'a seq \ 'a seq \ 'a seq"  (infixr ‹@@› 65)
  where "xs @@ ys \ sconc \ xs \ ys"

lemma sconc_UU [simp]: "UU @@ y = UU"
  by fixrec_simp

lemma sconc_cons [simp]: "(x ## xs) @@ y = x ## (xs @@ y)"
  by (cases "x = UU") simp_all

declare sconc_cons' [simp del]


subsubsection ‹‹sflat››

fixrec sflat :: "'a seq seq \ 'a seq"
where
  sflat_nil: "sflat \ nil = nil"
| sflat_cons': "x \ UU \ sflat \ (x ## xs) = x @@ (sflat \ xs)"

lemma sflat_UU [simp]: "sflat \ UU = UU"
  by fixrec_simp

lemma sflat_cons [simp]: "sflat \ (x ## xs) = x @@ (sflat \ xs)"
  by (cases "x = UU") simp_all

declare sflat_cons' [simp del]


subsubsection ‹‹szip››

fixrec szip :: "'a seq \ 'b seq \ ('a \ 'b) seq"
where
  szip_nil: "szip \ nil \ y = nil"
| szip_cons_nil: "x \ UU \ szip \ (x ## xs) \ nil = UU"
| szip_cons: "x \ UU \ y \ UU \ szip \ (x ## xs) \ (y ## ys) = (x, y) ## szip \ xs \ ys"

lemma szip_UU1 [simp]: "szip \ UU \ y = UU"
  by fixrec_simp

lemma szip_UU2 [simp]: "x \ nil \ szip \ x \ UU = UU"
  by (cases x) (simp_all, fixrec_simp)


subsection ‹‹scons›, ‹nil››

lemma scons_inject_eq: "x \ UU \ y \ UU \ x ## xs = y ## ys \ x = y \ xs = ys"
  by simp

lemma nil_less_is_nil: "nil \ x \ nil = x"
  by (cases x) simp_all


subsection ‹‹sfilter›, ‹sforall›, ‹sconc››

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

lemma sfiltersconc: "sfilter \ P \ (x @@ y) = (sfilter \ P \ x @@ sfilter \ P \ y)"
  apply (induct x)
  text ‹adm›
  apply simp
  text ‹base cases›
  apply simp
  apply simp
  text ‹main case›
  apply (rule_tac p = "P\a" in trE)
  apply simp
  apply simp
  apply simp
  done

lemma sforallPstakewhileP: "sforall P (stakewhile \ P \ x)"
  apply (simp add: sforall_def)
  apply (induct x)
  text ‹adm›
  apply simp
  text ‹base cases›
  apply simp
  apply simp
  text ‹main case›
  apply (rule_tac p = "P\a" in trE)
  apply simp
  apply simp
  apply simp
  done

lemma forallPsfilterP: "sforall P (sfilter \ P \ x)"
  apply (simp add: sforall_def)
  apply (induct x)
  text ‹adm›
  apply simp
  text ‹base cases›
  apply simp
  apply simp
  text ‹main case›
  apply (rule_tac p="P\a" in trE)
  apply simp
  apply simp
  apply simp
  done


subsection ‹Finite›

(*
  Proofs of rewrite rules for Finite:
    1. Finite nil    (by definition)
    2. \<not> Finite UU
    3. a \<noteq> UU \<Longrightarrow> Finite (a ## x) = Finite x
*)

lemma Finite_UU_a: "Finite x \ x \ UU"
  apply (rule impI)
  apply (erule Finite.induct)
   apply simp
  apply simp
  done

lemma Finite_UU [simp]: "\ Finite UU"
  using Finite_UU_a [where x = UU] by fast

lemma Finite_cons_a: "Finite x \ a \ UU \ x = a ## xs \ Finite xs"
  apply (intro strip)
  apply (erule Finite.cases)
  apply fastforce
  apply simp
  done

lemma Finite_cons: "a \ UU \ Finite (a##x) \ Finite x"
  apply (rule iffI)
  apply (erule (1) Finite_cons_a [rule_format])
  apply fast
  apply simp
  done

lemma Finite_upward: "Finite x \ x \ y \ Finite y"
  apply (induct arbitrary: y set: Finite)
  apply (case_tac y, simp, simp, simp)
  apply (case_tac y, simp, simp)
  apply simp
  done

lemma adm_Finite [simp]: "adm Finite"
  by (rule adm_upward) (rule Finite_upward)


subsection ‹Induction›

text ‹Extensions to Induction Theorems.›

lemma seq_finite_ind_lemma:
  assumes "\n. P (seq_take n \ s)"
  shows "seq_finite s \ P s"
  apply (unfold seq.finite_def)
  apply (intro strip)
  apply (erule exE)
  apply (erule subst)
  apply (rule assms)
  done

lemma seq_finite_ind:
  assumes "P UU"
    and "P nil"
    and "\x s1. x \ UU \ P s1 \ P (x ## s1)"
  shows "seq_finite s \ P s"
  apply (insert assms)
  apply (rule seq_finite_ind_lemma)
  apply (erule seq.finite_induct)
   apply assumption
  apply simp
  done

end