(* 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. ¬ Finite UU 3. a ≠ UU ⟹ 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